Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.RadiusIteration

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.coarseCaccioppoliBoundaryAlphaOfHeight_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (h : ℝ → ℝ → ℝ) {ρ₁ ρ₂ : ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hρ : ρ₁ < ρ₂) : 0 ≤ coarseCaccioppoliBoundaryAlphaOfHeight Q a s t C h ρ₁ ρ₂

theorem HCPolySupport.coarseCaccioppoliBoundaryCrossCoeffOfHeight_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) {ρ₁ ρ₂ : ℝ} (hC : 0 ≤ C) (hs : 0 < s) (hρ : ρ₁ < ρ₂) : 0 ≤ coarseCaccioppoliBoundaryCrossCoeffOfHeight Q a s C uL2Sq h ρ₁ ρ₂

theorem HCPolySupport.coarseCaccioppoli_absorb_cross_term {x α B : ℝ} (hx : 0 ≤ x) (hα : α ≤ 1 / 4) : α * x + B * √x ≤ 1 / 2 * x + B ^ 2

theorem HCPolySupport.coarseCaccioppoliRadiusIterationConst_nonneg (β : ℝ) : 0 ≤ coarseCaccioppoliRadiusIterationConst β

The deterministic radius-iteration constant is nonnegative.

theorem HCPolySupport.coarseCaccioppoliRadiusIterationConst_le_majorant_tsum (β : ℝ) (hβ : 0 ≤ β) : coarseCaccioppoliRadiusIterationConst β ≤ ∑' (n : ℕ), 2 ^ ⌈β⌉₊ * (↑(n + 2) ^ (2 * ⌈β⌉₊) * (1 / 2) ^ n)

Explicit polynomial-geometric majorant for the deterministic radius-iteration constant.

This is the scalar bottleneck isolated from the Caccioppoli proof: the final uniform public constant only has to bound this displayed series after taking the note exponent root.

theorem HCPolySupport.coarseCaccioppoliRadiusIterationConst_le_factorial_majorant (β : ℝ) (hβ : 0 ≤ β) : have k := ⌈β⌉₊; coarseCaccioppoliRadiusIterationConst β ≤ 4 * 2 ^ (3 * k) * ↑(2 * k).factorial

Factorial-geometric upper bound for the deterministic radius-iteration constant. This is the quantitative form needed to make the final Caccioppoli constant dimension-only: after the note exponent root, the remaining growth is controlled by σ * ceil β.

theorem HCPolySupport.coarseCaccioppoliRadiusIterationConst_le_power_majorant (β : ℝ) (hβ : 0 ≤ β) : have k := ⌈β⌉₊; coarseCaccioppoliRadiusIterationConst β ≤ 4 * 2 ^ (3 * k) * ↑(2 * k) ^ (2 * k)

Polynomial-geometric form of the radius-iteration constant. Compared with coarseCaccioppoliRadiusIterationConst_le_factorial_majorant, this replaces the factorial by the elementary power bound n! <= n^n.

theorem HCPolySupport.coarseCaccioppoli_radiusSequenceRecurrence_of_radiusRecurrence {F : ℝ → ℝ} {A β : ℝ} (hrec : CoarseCaccioppoliRadiusRecurrence F A β) : CoarseCaccioppoliRadiusSequenceRecurrence F A β

theorem HCPolySupport.coarseCaccioppoli_radius_iteration {F : ℝ → ℝ} {A β : ℝ} (hβ : 0 ≤ β) (hA : 0 ≤ A) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hrec : CoarseCaccioppoliRadiusRecurrence F A β) : F (1 / 3) ≤ A * coarseCaccioppoliRadiusIterationConst β

Quantitative radius iteration on [1/3, 1] with the 1/2-absorption used in the Chapter-3 coarse Caccioppoli proof.

theorem HCPolySupport.coarseCaccioppoli_radius_iteration_of_sequenceRecurrence {F : ℝ → ℝ} {A β : ℝ} (hβ : 0 ≤ β) (hA : 0 ≤ A) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hrec : CoarseCaccioppoliRadiusSequenceRecurrence F A β) : F (1 / 3) ≤ A * coarseCaccioppoliRadiusIterationConst β

Sequence-specialized version of the deterministic Chapter-3 radius iteration. This is the concrete interface used when the local bridge only produces the recursive inequality on the consecutive Chapter-3 radii (ρ_n, ρ_{n+1}).