IndisputableMonolith.Gravity.SevenGaps.DiracAlgebraContinuum

declarations in this module (25)

• def continuumMomentumFlux L64
• def continuumDiracDensity L69
• def sampledDynamicBracketSum L76
• def continuumWronskian L84
• lemma mesh_lt L89
• lemma mesh_step L94
• lemma mesh_le_one L98
• lemma mesh_nonneg L103
• lemma sample_mem_Icc L106
• lemma sample_mem_Icc_lt L113
• lemma Ioo_mesh_subset_Icc L117
• lemma exists_norm_bound_on_Icc L123
• theorem discrete_wronskian_mvt L133
• lemma continuous_continuumWronskian L172
• lemma wronskian_cell_error_abs L178
• theorem wronskian_rate_h_tendsto L203
• theorem forward_diff_mvt L401
• theorem forward_density_uniform L424
• theorem dynamicStructureProfile_eq_one_add_sq L499
• theorem bracket_HamDyn_shape L503
• theorem sampledDynamicBracketSum_scaled_eq L510
• theorem wronskian_times_uniform_error_tendsto_zero L525
• theorem dynamic_bracket_shape_continuum_limit L634
• theorem frozen_structure_differs_from_dynamic_id L727
• theorem frozen_continuum_density_differs_from_dynamic L733