Markov Property for the Energy Form

Proves that applying a normal contraction Φ does not increase the energy: E_λ(Φ ∘ G) ≤ E_λ(G). The proof proceeds in three layers: pointwise Lipschitz inequality, integral monotonicity via lintegral_mono, and assembly over archimedean and prime terms.

Reference: lamportform.tex, Section 5, lines 476–479.

Layer 1 — Pointwise norm inequality

theorem ConnesLean.nnnorm_sq_comp_le {Φ : ℝ → ℝ} (hΦ : IsNormalContraction Φ) (a b : ℝ) : ‖↑(Φ a) - ↑(Φ b)‖₊ ^ 2 ≤ ‖↑a - ↑b‖₊ ^ 2

Applying a normal contraction decreases the squared nnnorm (as NNReal): ‖Φ(a) - Φ(b)‖₊² ≤ ‖a - b‖₊².

Uses nnnorm_comp_le (from NormalContraction.lean) + NNReal.rpow_le_rpow.

Layer 1.5 — Pointwise bound for zeroExtend + translationOp

theorem ConnesLean.nnnorm_zeroExtend_comp_le {Φ : ℝ → ℝ} (hΦ : IsNormalContraction Φ) (G : ℝ → ℝ) (I : Set ℝ) (t u : ℝ) : ‖zeroExtend (liftReal (Φ ∘ G)) I u - translationOp t (zeroExtend (liftReal (Φ ∘ G)) I) u‖₊ ≤ ‖zeroExtend (liftReal G) I u - translationOp t (zeroExtend (liftReal G) I) u‖₊

Pointwise nnnorm bound after zeroExtend and translationOp rewriting. This bridges the abstract zeroExtend (liftReal ...) API to pointwise indicator values via zeroExtend_liftReal_comp and zeroExtend_liftReal.

Layer 2 — Integral inequality

theorem ConnesLean.lintegral_nnnorm_sq_comp_le {Φ : ℝ → ℝ} (hΦ : IsNormalContraction Φ) (G : ℝ → ℝ) (I : Set ℝ) (t : ℝ) : ∫⁻ (u : ℝ), ↑‖zeroExtend (liftReal (Φ ∘ G)) I u - translationOp t (zeroExtend (liftReal (Φ ∘ G)) I) u‖₊ ^ 2 ≤ ∫⁻ (u : ℝ), ↑‖zeroExtend (liftReal G) I u - translationOp t (zeroExtend (liftReal G) I) u‖₊ ^ 2

The L² norm integral decreases under a normal contraction: ∫ ‖G̃_Φ - S_t G̃_Φ‖₊² ≤ ∫ ‖G̃ - S_t G̃‖₊² for each fixed t.

Layer 3 — Assembly

theorem ConnesLean.archEnergyIntegrand_comp_le {Φ : ℝ → ℝ} (hΦ : IsNormalContraction Φ) (G : ℝ → ℝ) (L t : ℝ) : archEnergyIntegrand (liftReal (Φ ∘ G)) L t ≤ archEnergyIntegrand (liftReal G) L t

The archimedean energy integrand decreases under a normal contraction. Same weight (archWeight t).toNNReal, smaller lintegral.

theorem ConnesLean.archEnergyIntegral_comp_le {Φ : ℝ → ℝ} (hΦ : IsNormalContraction Φ) (G : ℝ → ℝ) (L : ℝ) : archEnergyIntegral (liftReal (Φ ∘ G)) L ≤ archEnergyIntegral (liftReal G) L

The archimedean energy integral decreases under a normal contraction. lintegral_mono over the outer t-integral.

theorem ConnesLean.primeEnergyTerm_comp_le {Φ : ℝ → ℝ} (hΦ : IsNormalContraction Φ) (G : ℝ → ℝ) (L : ℝ) (p m : ℕ) : primeEnergyTerm p m (liftReal (Φ ∘ G)) L ≤ primeEnergyTerm p m (liftReal G) L

Each prime energy term decreases under a normal contraction. Same weight (log p · p^{-m/2}).toNNReal, smaller lintegral.

theorem ConnesLean.totalPrimeEnergy_comp_le {Φ : ℝ → ℝ} (hΦ : IsNormalContraction Φ) (G : ℝ → ℝ) (L : ℝ) (p : ℕ) (cutoffLambda : ℝ) : totalPrimeEnergy p cutoffLambda (liftReal (Φ ∘ G)) L ≤ totalPrimeEnergy p cutoffLambda (liftReal G) L

The total prime energy decreases under a normal contraction. Finset.sum_le_sum over exponents.

Main theorem

theorem ConnesLean.energyForm_comp_normalContraction_le {Φ : ℝ → ℝ} (hΦ : IsNormalContraction Φ) (G : ℝ → ℝ) (cutoffLambda : ℝ) : energyForm cutoffLambda (liftReal (Φ ∘ G)) ≤ energyForm cutoffLambda (liftReal G)

Markov property: The energy form does not increase under normal contractions.

E_λ(Φ ∘ G) ≤ E_λ(G) for any normal contraction Φ.

Reference: lamportform.tex, Section 5, lines 476–479.

Corollary: absolute value

theorem ConnesLean.energyForm_abs_le (G : ℝ → ℝ) (cutoffLambda : ℝ) : energyForm cutoffLambda (liftReal fun (u : ℝ) => |G u|) ≤ energyForm cutoffLambda (liftReal G)

The energy of |G| is at most the energy of G. Special case of the Markov property with Φ = |·|.

Reference: lamportform.tex, line 478.