Iteration

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Generic De Giorgi iteration (level-volume decay)

This file isolates the purely analytic heart of the coupled Stampacchia estimate: starting from the geometric level-recursion inequality on the combined upper level volumes

(l − k)² · (a l)^{(d−2)/d} ≤ Crec · a k (for 0 ≤ k < l),

the combined level volume a tends to 0 along the truncation levels k_n := K (1 − 2^{-n}) as soon as the threshold K is chosen large enough.

The statement is fully abstract in the nonnegative "level-volume" function a : ℝ → ℝ; the geometric bookkeeping (α = d/(d−2), B = 4^α, Y_n = L^{-d} a(k_n)) reduces the recursion to the toolbox lemma iteration_geometric_decay_tendsto_zero.

noncomputable def HCPolySupport.deGiorgiLevel (K : ℝ) (n : ℕ) : ℝ

The truncation levels k_n = K (1 − 2^{-n}) used by the De Giorgi iteration.

Equations

• HCPolySupport.deGiorgiLevel K n = K * (1 - 2 ^ (-↑n))

@[simp]

theorem HCPolySupport.deGiorgiLevel_zero (K : ℝ) : deGiorgiLevel K 0 = 0

theorem HCPolySupport.deGiorgiLevel_nonneg {K : ℝ} (hK : 0 ≤ K) (n : ℕ) : 0 ≤ deGiorgiLevel K n

theorem HCPolySupport.deGiorgiLevel_lt {K : ℝ} (hK : 0 < K) (n : ℕ) : deGiorgiLevel K n < K

theorem HCPolySupport.deGiorgiLevel_strictMono {K : ℝ} (hK : 0 < K) : StrictMono (deGiorgiLevel K)

theorem HCPolySupport.deGiorgiLevel_succ_sub {K : ℝ} (n : ℕ) : deGiorgiLevel K (n + 1) - deGiorgiLevel K n = K * 2 ^ (-(↑n + 1))

The successive gap between De Giorgi levels: k_{n+1} − k_n = K·2^{-(n+1)}.

theorem HCPolySupport.four_rpow_eq (y : ℝ) : 4 ^ y = 2 ^ (2 * y)

Auxiliary: (4 : ℝ) ^ y = 2 ^ (2 * y) for real exponents.

theorem HCPolySupport.deGiorgiLevel_succ_sub_sq {K : ℝ} (n : ℕ) : (deGiorgiLevel K (n + 1) - deGiorgiLevel K n) ^ 2 = K ^ 2 * 4 ^ (-(↑n + 1))

The squared gap between successive De Giorgi levels, in 4-power form.

theorem HCPolySupport.deGiorgi_levelVolume_tendsto_zero {a : ℝ → ℝ} {Ld Crec K α β γ B : ℝ} (hnn : ∀ (k : ℝ), 0 ≤ a k) (hLd : 0 < Ld) (hCrec : 0 ≤ Crec) (hK : 0 < K) (hα1 : 1 < α) (hβ : β = α - 1) (hγα : γ * α = 1) (hB : B = 4 ^ α) (ha0 : a (deGiorgiLevel K 0) ≤ Ld) (hrec : ∀ (k l : ℝ), 0 ≤ k → k < l → (l - k) ^ 2 * a l ^ γ ≤ Crec * a k) (hKcond : (Crec / K ^ 2) ^ α * B * Ld ^ β ≤ B ^ (-(1 / β))) : Filter.Tendsto (fun (n : ℕ) => a (deGiorgiLevel K n)) Filter.atTop (nhds 0)

Generic De Giorgi iteration. If the combined upper-level volume a obeys the geometric level recursion and the threshold K is chosen so the leading iteration constant is admissible, then a tends to 0 along the truncation levels k_n = K(1 − 2^{-n}).

Here γ = (d−2)/d is the recursion exponent, α = d/(d−2) = 1/γ, β = α − 1, and B = 4^α.

theorem HCPolySupport.measure_eq_zero_of_toReal_tendsto {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {T : Set α} (hT : μ T ≠ ⊤) {b : ℕ → ℝ} (hle : ∀ (n : ℕ), (μ T).toReal ≤ b n) (hb : Filter.Tendsto b Filter.atTop (nhds 0)) : μ T = 0

A finite-measure set whose real mass is dominated by a null-tending sequence is null. Used to convert the level-volume decay into |{w > m + K}| = 0.