Normal Contractions and Real-to-Complex Bridge

Defines normal contractions (1-Lipschitz maps with Φ(0) = 0) and the liftReal embedding ℝ → ℂ. Provides bridge lemmas connecting real-valued indicator functions to the ℂ-typed zeroExtend/energyForm API.

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

Normal contractions

structure ConnesLean.IsNormalContraction (Φ : ℝ → ℝ) : Prop

A normal contraction is a map Φ : ℝ → ℝ with Φ(0) = 0 and |Φ(a) - Φ(b)| ≤ |a - b| for all a, b (i.e., 1-Lipschitz).

Reference: lamportform.tex, lines 476–479.

• map_zero : Φ 0 = 0
• lipschitz : LipschitzWith 1 Φ

Basic instances

theorem ConnesLean.isNormalContraction_abs : IsNormalContraction fun (x : ℝ) => |x|

The absolute value function |·| is a normal contraction. Uses lipschitzWith_one_norm (norm is 1-Lipschitz) and Real.norm_eq_abs.

theorem ConnesLean.isNormalContraction_id : IsNormalContraction id

The identity function is a normal contraction.

Properties of normal contractions

theorem ConnesLean.IsNormalContraction.bound {Φ : ℝ → ℝ} (hΦ : IsNormalContraction Φ) (a : ℝ) : |Φ a| ≤ |a|

A normal contraction is bounded by the identity: |Φ(a)| ≤ |a|. Set b = 0 in the Lipschitz condition and use Φ(0) = 0.

theorem ConnesLean.IsNormalContraction.measurable {Φ : ℝ → ℝ} (hΦ : IsNormalContraction Φ) : Measurable Φ

A normal contraction is measurable (Lipschitz → continuous → measurable).

Indicator composition

theorem ConnesLean.indicator_comp_normalContraction {Φ : ℝ → ℝ} (hΦ : IsNormalContraction Φ) (G : ℝ → ℝ) (I : Set ℝ) : I.indicator (Φ ∘ G) = Φ ∘ I.indicator G

Composing an indicator with a zero-preserving function commutes: I.indicator (Φ ∘ G) = Φ ∘ (I.indicator G) when Φ(0) = 0.

This is a direct application of Set.indicator_comp_of_zero.

The liftReal embedding

def ConnesLean.liftReal (G : ℝ → ℝ) : ℝ → ℂ

Embed a real-valued function into ℝ → ℂ via the canonical coercion. This is used to feed real-valued functions into the ℂ-typed energy form.

Equations

• ConnesLean.liftReal G u = ↑(G u)

@[simp]

theorem ConnesLean.liftReal_apply (G : ℝ → ℝ) (u : ℝ) : liftReal G u = ↑(G u)

Bridge lemmas: zeroExtend ↔ liftReal

theorem ConnesLean.zeroExtend_liftReal (G : ℝ → ℝ) (I : Set ℝ) : zeroExtend (liftReal G) I = fun (u : ℝ) => ↑(I.indicator G u)

Zero-extending a lifted real function factors through the real indicator: zeroExtend (liftReal G) I u = ↑(I.indicator G u).

Uses Set.indicator_comp_of_zero with Complex.ofReal_zero.

theorem ConnesLean.zeroExtend_liftReal_comp {Φ : ℝ → ℝ} (hΦ : IsNormalContraction Φ) (G : ℝ → ℝ) (I : Set ℝ) : zeroExtend (liftReal (Φ ∘ G)) I = fun (u : ℝ) => ↑(Φ (I.indicator G u))

Key bridge lemma: zero-extending a lifted composition factors through the real indicator composed with Φ: zeroExtend (liftReal (Φ ∘ G)) I = fun u => ↑(Φ (I.indicator G u)).

This is the critical connection between zeroExtend (typed ℝ → ℂ) and the real-valued indicator needed for Lipschitz bounds in PR B.

Proof: two applications of Set.indicator_comp_of_zero — first for Φ (via hΦ.map_zero), then for (↑· : ℝ → ℂ) (via Complex.ofReal_zero).

Norm bridge lemmas

theorem ConnesLean.liftReal_sub_apply (a b : ℝ → ℝ) (u : ℝ) : liftReal a u - liftReal b u = ↑(a u - b u)

Subtraction commutes with liftReal: liftReal a u - liftReal b u = ↑(a u - b u).

theorem ConnesLean.nnnorm_liftReal_sub (a b : ℝ → ℝ) (u : ℝ) : ‖liftReal a u - liftReal b u‖₊ = ‖a u - b u‖₊

The nnnorm bridge: ‖liftReal a u - liftReal b u‖₊ = ‖a u - b u‖₊. Reduces ℂ-valued nnnorm to ℝ-valued nnnorm via Complex.ofReal_sub and Complex.nnnorm_real.

Pointwise norm inequality under contraction

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

Pointwise nnnorm inequality: applying a normal contraction decreases nnnorms. ‖↑(Φ a) - ↑(Φ b)‖₊ ≤ ‖↑a - ↑b‖₊ in ℂ.

This is the key ingredient for lintegral_mono in the Markov property.