Coarse-graining support: Support.Book.Ch05.Theorems.Section55.AnnealedImprovement

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

One annealed improvement step

This file formalizes the scalar iteration step from Section 5.5. The first bridge below is a windowed version of the Section 5.4 pigeonhole lemma, obtained by applying the existing result to the scale-normalized law.

theorem HCPolySupport.Book.Ch05.Section55.windowPigeonhole_homogenizationScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta sigma : ℝ} (hdelta_pos : 0 < delta) (hdelta_le : delta ≤ 1 / 2) (hsigma_pos : 0 < sigma) (hsigma_le : sigma ≤ 1 / 2) {k M h : ℕ} (hsep : ⌈2 * delta⁻¹ * |Real.log sigma|⌉₊ * h ≤ M) : (∃ (n : ℕ), k + h ≤ n ∧ n ≤ k + M ∧ hP.barSigmaAtScale hStruct ↑(n - h) ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑n ∧ (hP.barSigmaStarAtScale hStruct ↑(n - h))⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑n)⁻¹) ∨ thetaAtScale hP hStruct ↑(k + M) ≤ sigma * thetaAtScale hP hStruct ↑k

Pigeonhole on an arbitrary scale window [k, k + M].

Either there is a good subwindow of length h, or the annealed contrast has already contracted from scale k to scale k + M.

theorem HCPolySupport.Book.Ch05.Section55.oneStepAnnealedImprovement_homogenizationScale_of_auxiliary {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ), 0 < C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.params = params → ∀ {delta sigma : ℝ}, 0 < delta → delta ≤ 1 / 2 → 0 < sigma → sigma ≤ 1 / 2 → ∀ {k M h : ℕ}, ⌈2 * delta⁻¹ * |Real.log sigma|⌉₊ * h ≤ M → C * ↑params.xi * Real.log (2 + delta⁻¹ * ↑params.xi * widetildeThetaAtScale P 0 hP4) ≤ ↑h → C * delta.rpow (1 / 4) ≤ sigma / 2 → C * Real.rpow 3 (-Section53.JUpperBoundCoarseFluctuations.coarseFluctuationBeta params * ↑h) * widetildeThetaAtScale P 0 hP4 ≤ sigma / 2 → thetaAtScale hP hStruct ↑(k + M + h) ≤ 1 + sigma * thetaAtScale hP hStruct ↑k

The core Section 5.5 improvement step with the auxiliary gap h and smallness conditions left explicit.

The final note-facing lemma will choose δ and h from σ; this theorem locks down the mathematical iteration once those scalar choices are supplied.

theorem HCPolySupport.Book.Ch05.Section55.oneStepAnnealedImprovement_homogenizationScale_of_discrete_gap {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ), 0 < C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.params = params → ∀ {delta sigma : ℝ}, 0 < delta → delta ≤ 1 / 2 → 0 < sigma → sigma ≤ 1 / 2 → ∀ {k N h : ℕ}, k ≤ N → (⌈2 * delta⁻¹ * |Real.log sigma|⌉₊ + 1) * h ≤ N - k → C * ↑params.xi * Real.log (2 + delta⁻¹ * ↑params.xi * widetildeThetaAtScale P 0 hP4) ≤ ↑h → C * delta.rpow (1 / 4) ≤ sigma / 2 → C * Real.rpow 3 (-Section53.JUpperBoundCoarseFluctuations.coarseFluctuationBeta params * ↑h) * widetildeThetaAtScale P 0 hP4 ≤ sigma / 2 → thetaAtScale hP hStruct ↑N ≤ 1 + sigma * thetaAtScale hP hStruct ↑k

The auxiliary improvement step restated with the final endpoint N and the exact discrete gap condition used in the manuscript proof.

theorem HCPolySupport.Book.Ch05.Section55.oneStepAnnealedImprovement_homogenizationScale {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ), 0 < C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.params = params → ∀ {sigma : ℝ}, 0 < sigma → sigma ≤ 1 / 2 → ∀ {k N : ℕ}, k ≤ N → C * ↑params.xi * sigma⁻¹ ^ 4 * |Real.log sigma| * Real.log (2 + sigma⁻¹ ^ 4 * ↑params.xi * widetildeThetaAtScale P 0 hP4) ≤ ↑(N - k) → thetaAtScale hP hStruct ↑N ≤ 1 + sigma * thetaAtScale hP hStruct ↑k

One improvement step for the annealed scalar contrast.

This is the note-facing Section 5.5 form, with the constant chosen from the parameter record before the law, the window, and σ. The Lean statement uses (σ⁻¹)^4 for the manuscript factor σ^{-4}.