IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Tendsto4D

declarations in this module (19)

• def areaAlong L33
• def kerAlong L36
• theorem areaAlong_eq L39
• theorem kerAlong_eq L46
• theorem areaAlong_zero L54
• theorem kerAlong_zero L59
• theorem kerAlong_axis_zero L64
• theorem kerAlong_gauge_zero L69
• def kerM2Coeff L75
• theorem tendsto_kerAlong_div_sq L81
• theorem continuous_areaAlong L153
• theorem tendsto_slot_product L166
• theorem m2SlotCoeff_eq_area_kerM2 L185
• theorem tendsto_transportedSlotTerm_div_sq L193
• theorem tendsto_foldAlong_div_sq L217
• theorem FoldAlongM2Tendsto_of_axisTTPlus L246
• theorem FoldAlongM2Tendsto_of_decoyGauge L251
• theorem FoldAlongM2Tendsto_axisTTPlus_holds L256
• theorem FoldAlongM2Tendsto_decoyGauge_holds L260