Constant Function in Form Domain

Shows that the constant function 1 is in the energy form domain, applies the energy splitting to it, and establishes indicator complement identities.

Reference: lamportform.tex, Proposition 10, Steps 1–3 (lines 1312–1370).

Section 1: Inner integral bound for constant function

theorem ConnesLean.inner_integral_one_le {L t : ℝ} (_hL : 0 < L) (ht : 0 < t) (_htL : t < 2 * L) : ∫⁻ (u : ℝ), ↑‖zeroExtend 1 (logInterval L) u - translationOp t (zeroExtend 1 (logInterval L)) u‖₊ ^ 2 ≤ ENNReal.ofReal (2 * t)

For 0 < t < 2L, the L² norm of φ - S_t φ is at most 2t, where φ = zeroExtend 1 I. The function disagrees with its translate only on the symmetric difference I Δ (I+t), which has measure 2t.

Section 2: Archimedean energy finiteness

theorem ConnesLean.archEnergyIntegral_one_lt_top {L : ℝ} (hL : 0 < L) : archEnergyIntegral 1 L < ⊤

The archimedean energy integral of the constant function is finite. Combines archWeight(t) ≤ exp(t/2)/(2t) with inner integral ≤ 2t to get integrand ≤ exp(L), then integrates over (0, 2L).

Section 3: Constant function in form domain

theorem ConnesLean.inner_integral_one_lt_top (L shift : ℝ) : ∫⁻ (u : ℝ), ↑‖zeroExtend 1 (logInterval L) u - translationOp shift (zeroExtend 1 (logInterval L)) u‖₊ ^ 2 < ⊤

The inner integral of the constant function is finite for any shift. The integrand ≤ 1 on I ∪ (I + shift), both of which have measure 2L.

theorem ConnesLean.constant_in_formDomain {cutoffLambda : ℝ} (hLam : 1 < cutoffLambda) : 1 ∈ formDomain cutoffLambda

The constant function 1 belongs to the form domain D(E_λ): its energy form is finite. The archimedean part is finite by archEnergyIntegral_one_lt_top, and the prime part is a finite sum of finite terms.

Section 4: Splitting applied to constant

theorem ConnesLean.splitting_applied_to_constant {cutoffLambda : ℝ} (hLam : 1 < cutoffLambda) (inv : EnergyFormSplit cutoffLambda) : inv.B.indicator 1 ∈ formDomain cutoffLambda ∧ (logInterval (Real.log cutoffLambda) \ inv.B).indicator 1 ∈ formDomain cutoffLambda ∧ energyForm cutoffLambda 1 = energyForm cutoffLambda (inv.B.indicator 1) + energyForm cutoffLambda ((logInterval (Real.log cutoffLambda) \ inv.B).indicator 1)

The energy of the constant function splits across any EnergyFormSplit. Direct application of EnergyFormSplit.split with G = 1.

Section 5: Indicator complement arithmetic

theorem ConnesLean.indicator_complement_sum {B I : Set ℝ} (hB : B ⊆ I) (u : ℝ) : zeroExtend (B.indicator 1) I u + zeroExtend ((I \ B).indicator 1) I u = zeroExtend 1 I u

For B ⊆ I, the zero-extended indicators of B and I \ B sum to the zero-extended constant function: 1_B + 1_{I\B} = 1_I pointwise.

Uses Set.indicator_indicator to simplify I.indicator (B.indicator f) = (I ∩ B).indicator f, which reduces to B.indicator f when B ⊆ I.

theorem ConnesLean.indicator_complement_disjoint {B I : Set ℝ} (hB : B ⊆ I) (u : ℝ) : zeroExtend (B.indicator 1) I u * zeroExtend ((I \ B).indicator 1) I u = 0

For any B, the zero-extended indicators of B and I \ B have disjoint support: their product is zero at every point.

Since B and I \ B are disjoint, at most one indicator is nonzero at any point, making their product zero.

Section 6: Soundness tests