Energy Equality for Disjoint Indicators

Establishes that the energy form equality from Stage 6C, combined with the norm inequality from Stage 6D-i, forces component-wise equality of the archimedean energy integrands, and by continuity, of the inner integrals everywhere on (0, 2L).

Reference: lamportform.tex, Proposition 10, Steps 8–9 (lines 1391–1425).

Section 1: ENNReal cancellation helper

Section 2: Archimedean energy integral equality

theorem ConnesLean.archEnergyIntegral_indicator_eq {cutoffLambda : ℝ} (hLam : 1 < cutoffLambda) (inv : EnergyFormSplit cutoffLambda) : archEnergyIntegral 1 (Real.log cutoffLambda) = archEnergyIntegral (inv.B.indicator 1) (Real.log cutoffLambda) + archEnergyIntegral ((logInterval (Real.log cutoffLambda) \ inv.B).indicator 1) (Real.log cutoffLambda)

Archimedean energy integral equality. The archimedean energy of the constant function equals the sum of energies of complementary indicators.

Proof: the full energy form equality (Stage 6C) + component-wise inequalities (Stage 6D-i) + ENNReal cancellation.

Reference: lamportform.tex, Proposition 10, Step 8 (line 1391).

Section 3: Archimedean energy integrand ae equality

theorem ConnesLean.archEnergyIntegrand_indicator_ae_eq {cutoffLambda : ℝ} (hLam : 1 < cutoffLambda) (inv : EnergyFormSplit cutoffLambda) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 (2 * Real.log cutoffLambda)), archEnergyIntegrand 1 (Real.log cutoffLambda) t = archEnergyIntegrand (inv.B.indicator 1) (Real.log cutoffLambda) t + archEnergyIntegrand ((logInterval (Real.log cutoffLambda) \ inv.B).indicator 1) (Real.log cutoffLambda) t

The archimedean energy integrands agree a.e. on (0, 2L): archEnergyIntegrand(1, t) = archEnergyIntegrand(B, t) + archEnergyIntegrand(Bc, t).

Proof: pointwise ≤ (from 6D-i) + integral equality (Theorem 1) + ae_eq_of_ae_le_of_lintegral_le.

Reference: lamportform.tex, Proposition 10, Step 8.

Section 4: Inner integral definition and ae equality

def ConnesLean.innerIntegral (G : ℝ → ℂ) (L t : ℝ) : ENNReal

The inner L² translation integral: ∫ ‖φ̃(u) - S_t φ̃(u)‖₊² du where φ̃ = zeroExtend G I. This is the second factor of archEnergyIntegrand G L t = weight(t) * innerIntegral G L t.

Equations

• One or more equations did not get rendered due to their size.

theorem ConnesLean.inner_integral_indicator_ae_eq {cutoffLambda : ℝ} (hLam : 1 < cutoffLambda) (inv : EnergyFormSplit cutoffLambda) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 (2 * Real.log cutoffLambda)), innerIntegral 1 (Real.log cutoffLambda) t = innerIntegral (inv.B.indicator 1) (Real.log cutoffLambda) t + innerIntegral ((logInterval (Real.log cutoffLambda) \ inv.B).indicator 1) (Real.log cutoffLambda) t

The inner integrals agree a.e. on (0, 2L): II(1, t) = II(B, t) + II(Bc, t) for a.e. t ∈ (0, 2L).

From the integrand a.e. equality w(t) * II(1) = w(t) * (II(B) + II(Bc)) by cancelling the positive weight w(t).

Reference: lamportform.tex, Proposition 10, Step 8.

Section 5: Continuity and everywhere equality

theorem ConnesLean.inner_integral_indicator_everywhere_eq {cutoffLambda : ℝ} (hLam : 1 < cutoffLambda) (inv : EnergyFormSplit cutoffLambda) (t : ℝ) : t ∈ Set.Ioo 0 (2 * Real.log cutoffLambda) → innerIntegral 1 (Real.log cutoffLambda) t = innerIntegral (inv.B.indicator 1) (Real.log cutoffLambda) t + innerIntegral ((logInterval (Real.log cutoffLambda) \ inv.B).indicator 1) (Real.log cutoffLambda) t

Inner integral equality everywhere on (0, 2L). The inner integrals II(1, t) = II(B, t) + II(Bc, t) for all t ∈ (0, 2L).

Proof: each side is continuous (by translation_norm_sq_continuous), they agree a.e. (from weight cancellation), and continuous functions that agree a.e. on an open set agree everywhere (by eqOn_of_ae_eq).

Reference: lamportform.tex, Proposition 10, Step 9 (line 1411).

Section 6: Soundness tests