High-contrast homogenization: Provider.Quenched.SmallContrastBootstrapSmallness

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The bootstrap smallness of the hatted carrier

The recursion of the small-contrast argument runs on F(n) = d(hatΘ_n − 1) and needs a uniform smallness F ≤ δ over the whole range it iterates on. The only smallness the proposition assumes is Euclidean and at generation zero: Θ_0 − 1 ≤ c_*.

The transfer is the adapted-to-Euclidean adapter run in the descending direction: at generation n compare the adapted mean with the annealed block of the centered cube a fixed gap of scales earlier. The comparison error carries 3^{−gap} and is absorbed multiplicatively; the Euclidean hatted defect at the earlier cube is below c_* because the annealed intrinsic contrast is antitone and dominates the hatted carrier. The absorbed size is c·|𝐄 : 𝐀(□_k)|, and the second factor is the generation-free Euclidean reference ratio, so a single gap — logarithmic in the law constants — serves every generation past the source burn.

Nothing in this file is a window estimate: the account, the coupled window and the profile caps play no role. What is used is the two-sided Euclidean adapter, the Dagger envelope through the reference ratio, the tilt scalarization, and the annealed antitone comparison.

theorem HCPolySupport.HighContrast.Quenched.transferGauge_le_bar {g K : ℝ} (hg : g ∈ Set.Ico 0 1) {j : ℤ} (hj : 0 ≤ j) : transferGauge g K j ≤ (1 - g)⁻¹ * (1 + K ^ 2) ^ g

The source gauge of the adapted-to-Euclidean adapter is bounded, at every nonnegative scale, by its value at scale zero.

noncomputable def HCPolySupport.HighContrast.Quenched.bootstrapAdapterFactor {d : ℕ} (Cd g K : ℝ) (E : BlockMat d) (mAl : Mat d) : ℝ

The law-side factor of the bootstrap adapter error: the grid eccentricity, the source-gauge cap and the Euclidean reference ratio.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Quenched.exists_bootstrap_tilt_bound (d : ℕ) (hd : 2 ≤ d) (g : ℝ) (hg : g ∈ Set.Ico 0 1) : ∃ (CB : ℝ), 0 < CB ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P g E Ψ K S → ∀ (Cd : ℝ), max 1 (12 * ↑d * √↑d) ≤ Cd → ∀ (sK : ℤ), 0 ≤ sK → growthBar K ≤ 3 ^ sK → ∀ (lq : ℤ), ↑(kZero d) ≤ lq → ∀ (mAl : Mat d), Matrix.PosDef mAl → ∀ (sigma cStar : ℝ), annealedContrast P 0 - 1 ≤ cStar → ∀ (gap : ℤ), 1 ≤ gap → CB * bootstrapAdapterFactor Cd g K E mAl * 3 ^ (-↑gap) ≤ sigma → ∀ (n : ℤ), sK + 1 + gap ≤ n → ↑d * (adaptedHattedContrast P (roundedGrid lq mAl) n - 1) ≤ ↑d * bootstrapTiltPolynomial sigma (↑d * cStar)

The bootstrap tilt bound. With the alignment-free triadic gap chosen so that the absorbed adapter error is below σ, the hatted defect of the adapted mean at every generation past the source burn plus the gap is bounded by the tilt polynomial at σ and d c_*.