De Giorgi preiter to recurrence
DeGiorgi.deGiorgi_preiter_to_recurrence
Plain-language statement
Rewrite the one-step estimate on canonical radii and levels into the standard nonlinear recurrence.
Exact Lean statement
theorem deGiorgi_preiter_to_recurrence
{Aseq : ℕ → ℝ} {d : ℕ}
{K lamStar : ℝ} (hLamStar : 0 < lamStar)
(hpre :
∀ n,
Aseq (n + 1) ≤
K / ((deGiorgiRadius n - deGiorgiRadius (n + 1)) ^ 2 *
(deGiorgiLevel lamStar (n + 1) - deGiorgiLevel lamStar n) ^ (4 / (d : ℝ))) *
Aseq n ^ (1 + 2 / (d : ℝ))) :
∀ n,
Aseq (n + 1) ≤
deGiorgiRecurrenceCoeff d K lamStar *
deGiorgiRecurrenceBase d ^ n *
Aseq n ^ (1 + 2 / (d : ℝ))Formal artifact
Lean source
theorem deGiorgi_preiter_to_recurrence {Aseq : ℕ → ℝ} {d : ℕ} {K lamStar : ℝ} (hLamStar : 0 < lamStar) (hpre : ∀ n, Aseq (n + 1) ≤ K / ((deGiorgiRadius n - deGiorgiRadius (n + 1)) ^ 2 * (deGiorgiLevel lamStar (n + 1) - deGiorgiLevel lamStar n) ^ (4 / (d : ℝ))) * Aseq n ^ (1 + 2 / (d : ℝ))) : ∀ n, Aseq (n + 1) ≤ deGiorgiRecurrenceCoeff d K lamStar * deGiorgiRecurrenceBase d ^ n * Aseq n ^ (1 + 2 / (d : ℝ)) := by intro n have htwo_pos : 0 < (2 : ℝ) := by positivity have hhalf : (1 / 2 : ℝ) = (2 : ℝ) ^ (-(1 : ℝ)) := by rw [Real.rpow_neg (by positivity), Real.rpow_one] norm_num have hrad : (deGiorgiRadius n - deGiorgiRadius (n + 1)) ^ 2 = (2 : ℝ) ^ (-(2 * n + 6 : ℝ)) := by rw [deGiorgiRadius_gap, pow_two, ← pow_add] have hnat : n + 3 + (n + 3) = 2 * n + 6 := by omega rw [hnat, ← Real.rpow_natCast] rw [hhalf] rw [← Real.rpow_mul htwo_pos.le] rw [show (-(1 : ℝ)) * (((2 * n + 6 : ℕ) : ℝ)) = -(2 * (n : ℝ) + 6) by norm_num [Nat.cast_add, Nat.cast_mul]] have htail_rpow : ((1 / 2 : ℝ) ^ (n + 2)) ^ (4 / (d : ℝ)) = (2 : ℝ) ^ (-((n + 2 : ℝ) * (4 / (d : ℝ)))) := by rw [← Real.rpow_natCast] rw [hhalf] rw [show (((n + 2 : ℕ) : ℝ) = (n : ℝ) + 2) by norm_num] calc (((2 : ℝ) ^ (-(1 : ℝ))) ^ ((n : ℝ) + 2)) ^ (4 / (d : ℝ)) = ((2 : ℝ) ^ ((-(1 : ℝ)) * ((n : ℝ) + 2))) ^ (4 / (d : ℝ)) := by rw [← Real.rpow_mul htwo_pos.le] _ = (2 : ℝ) ^ (((-(1 : ℝ)) * ((n + 2 : ℝ))) * (4 / (d : ℝ))) := by rw [← Real.rpow_mul htwo_pos.le] _ = (2 : ℝ) ^ (-((n + 2 : ℝ) * (4 / (d : ℝ)))) := by congr 1 ring have hlev : (deGiorgiLevel lamStar (n + 1) - deGiorgiLevel lamStar n) ^ (4 / (d : ℝ)) = lamStar ^ (4 / (d : ℝ)) * (2 : ℝ) ^ (-((n + 2 : ℝ) * (4 / (d : ℝ)))) := by rw [deGiorgiLevel_gap] rw [Real.mul_rpow hLamStar.le (by positivity)] rw [htail_rpow] have hden : (deGiorgiRadius n - deGiorgiRadius (n + 1)) ^ 2 * (deGiorgiLevel lamStar (n + 1) - deGiorgiLevel lamStar n) ^ (4 / (d : ℝ)) = lamStar ^ (4 / (d : ℝ)) * (2 : ℝ) ^ (-(6 + 8 / (d : ℝ) + n * (2 + 4 / (d : ℝ)))) := by rw [hrad, hlev] calc (2 : ℝ) ^ (-(2 * n + 6 : ℝ)) * (lamStar ^ (4 / (d : ℝ)) * (2 : ℝ) ^ (-((n + 2 : ℝ) * (4 / (d : ℝ))))) = lamStar ^ (4 / (d : ℝ)) * ((2 : ℝ) ^ (-(2 * n + 6 : ℝ)) * (2 : ℝ) ^ (-((n + 2 : ℝ) * (4 / (d : ℝ))))) := by ring _ = lamStar ^ (4 / (d : ℝ)) * (2 : ℝ) ^ (-(2 * n + 6 : ℝ) + -((n + 2 : ℝ) * (4 / (d : ℝ)))) := by rw [← Real.rpow_add htwo_pos] _ = lamStar ^ (4 / (d : ℝ)) * (2 : ℝ) ^ (-(6 + 8 / (d : ℝ) + n * (2 + 4 / (d : ℝ)))) := by congr 1 ring_nf have hrec := hpre n calc Aseq (n + 1) ≤ K / ((deGiorgiRadius n - deGiorgiRadius (n + 1)) ^ 2 * (deGiorgiLevel lamStar (n + 1) - deGiorgiLevel lamStar n) ^ (4 / (d : ℝ))) * Aseq n ^ (1 + 2 / (d : ℝ)) := hrec _ = deGiorgiRecurrenceCoeff d K lamStar * deGiorgiRecurrenceBase d ^ n * Aseq n ^ (1 + 2 / (d : ℝ)) := by rw [hden] rw [deGiorgiRecurrenceCoeff, deGiorgiRecurrenceBase] rw [div_eq_mul_inv] rw [show (lamStar ^ (4 / (d : ℝ)) * (2 : ℝ) ^ (-(6 + 8 / (d : ℝ) + n * (2 + 4 / (d : ℝ)))))⁻¹ = ((2 : ℝ) ^ (-(6 + 8 / (d : ℝ) + n * (2 + 4 / (d : ℝ)))))⁻¹ * (lamStar ^ (4 / (d : ℝ)))⁻¹ by rw [_root_.mul_inv_rev]] rw [Real.rpow_neg htwo_pos.le, Real.rpow_neg hLamStar.le] simp only [inv_inv] have hsplitpow : (2 : ℝ) ^ (6 + 8 / (d : ℝ) + n * (2 + 4 / (d : ℝ))) = (2 : ℝ) ^ (6 + 8 / (d : ℝ)) * (2 : ℝ) ^ (n * (2 + 4 / (d : ℝ))) := by rw [← Real.rpow_add htwo_pos] rw [hsplitpow] rw [show n * (2 + 4 / (d : ℝ)) = (2 + 4 / (d : ℝ)) * n by ring] rw [Real.rpow_mul htwo_pos.le, Real.rpow_natCast] ac_rfl- Project
- DeGiorgi
- License
- Apache-2.0
- Commit
- 4c1b3077d378
- Source
- DeGiorgi/DeGiorgiIteration/Recurrence.lean:229-325
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Ae eq of tendsto e Lp Norm sub
BareFunction.ae_eq_of_tendsto_eLpNorm_sub
Plain-language statement
Lp limit uniqueness: if f_n → g₁ and f_n → g₂ in eLpNorm, then g₁ =ᵐ g₂.
Source project: DeGiorgi
Person-level attribution pending.
E Lp Norm pi le sum component
BareFunction.eLpNorm_pi_le_sum_component
Plain-language statement
Vector eLpNorm ≤ sum of component eLpNorms for Pi-valued functions. Uses eLpNorm_mono_real for the pointwise bound together with eLpNorm_sum_le for ℝ-valued functions, avoiding Pi instance synthesis.
Source project: DeGiorgi
Person-level attribution pending.
Mem Lp of tendsto e Lp Norm
BareFunction.memLp_of_tendsto_eLpNorm
Plain-language statement
If f n → g in eLpNorm and each f n ∈ Lp, then g ∈ Lp, provided g is AEStronglyMeasurable. Avoids the Lp type entirely. The key observation: eLpNorm (f n - g) → 0 means eLpNorm (f N - g) < 1 for some N. Then eLpNorm g ≤ eLpNorm (f N - g) + eLpNorm (f N) < ∞.
Source project: DeGiorgi
Person-level attribution pending.