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

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

noncomputable def HCPolySupport.coarseCaccioppoliStandardRadiusTheta (β : ℝ) : ℝ

Geometric ratio used in the standard beta-dependent radius iteration. It is close enough to 1 that the geometric loss has ratio bounded away from 1, but 1 - theta is still explicitly comparable to (max 1 beta)⁻¹.

Equations

• HCPolySupport.coarseCaccioppoliStandardRadiusTheta β = 1 - (4 * max 1 β)⁻¹

noncomputable def HCPolySupport.coarseCaccioppoliStandardRadiusIterationConst (β : ℝ) : ℝ

The beta-dependent radius-iteration constant from the standard hole-filling proof. The factor 3 comes from summing a geometric series with ratio at most 2 / 3.

Equations

• HCPolySupport.coarseCaccioppoliStandardRadiusIterationConst β = 3 * (1 - HCPolySupport.coarseCaccioppoliStandardRadiusTheta β).rpow (-β) * (2 / 3).rpow (-β)

theorem HCPolySupport.coarseCaccioppoliStandardRadiusIterationConst_nonneg {β : ℝ} (hβ : 0 ≤ β) : 0 ≤ coarseCaccioppoliStandardRadiusIterationConst β

theorem HCPolySupport.coarseCaccioppoliStandardRadiusIterationConst_eq_growth (β : ℝ) : coarseCaccioppoliStandardRadiusIterationConst β = 3 * (6 * max 1 β).rpow β

Closed scalar form of the standard radius-iteration constant. This is the piece needed by the final Caccioppoli scalar envelope: the beta-dependent iteration costs exactly a (6 * max 1 beta)^beta factor up to the harmless front constant 3.

theorem HCPolySupport.coarseCaccioppoli_sigma_mul_standardRadiusIterationConst_root_le {s t : ℝ} (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : have σ := coarseCaccioppoliSigma s t; have p := 2 + 4 * s / σ; σ * (coarseCaccioppoliStandardRadiusIterationConst (coarseCaccioppoliBeta s t)).rpow p⁻¹ ≤ 36

After taking the note-exponent root, the beta-dependent radius-iteration constant has a dimensionless scalar bound. This is the scalar cancellation used by the note-facing Caccioppoli constant: the apparent beta growth is absorbed by sigma * beta <= 2.

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

Standard beta-dependent radius iteration on [1/3,1]. Unlike the fixed deterministic radius sequence, this is the note-facing hole-filling estimate: the iteration constant grows like (C * max 1 beta)^beta.