Documentation

LeanPool.HighContrastHomogenization.Provider.Quenched.SmallContrastBootstrapReverseAdapter

High-contrast homogenization: Provider.Quenched.SmallContrastBootstrapReverseAdapter #

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

The reverse Euclidean adapter with a decaying absorbed size #

The endgame runs the adapted-to-Euclidean adapter in the reverse direction: the annealed block of the outer cube β–‘_m is compared with the adapted mean at the corrected halfway scale n, and the comparison error must decay in m βˆ’ n with a constant that does not move with the generation.

Two ingredients make the absorbed size cΒ·|𝐄 : E_n^q| uniform. The first is the reference ratio at the selection grid: the Dagger envelope on the adapted cell, the sharp reversal, and 𝐄 ≀ ΞΊ_𝐄 𝐄_# bound |𝐄 : E_n^q| by ΞΊ_𝐄 Β· C(K) Β· B_q Β· 3^{gG}, where G is the grid's enclosure enlargement β€” the same chain the bootstrap uses on the Euclidean grid, at a general witness and a general enlargement. The second is the source gauge, bounded at every nonnegative scale by its value at scale zero.

The result is the pair of inputs the corrected tilt transfer consumes: the Loewner adapter itself and a decaying bound cΒ·|𝐄 : E_n^q| ≀ CB Β· factor Β· 3^{βˆ’(mβˆ’n)} on the absorbed size. Taking m βˆ’ n large enough turns the second into the unit cap Ξ· ≀ 1; taking A β‰₯ (9/2)Β·CBΒ·factor turns it into the error clause.

source
noncomputable def HCPolySupport.HighContrast.Quenched.gridReferenceRatio {d : β„•} (Cd g K : ℝ) (E : BlockMat d) (mAl : Mat d) (G : β„•) :
ℝ

The reference ratio at a rounded selection grid whose adapted cells are enclosed with enlargement G.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.HighContrast.Quenched.blockSize_reference_adaptedMean_le {d : β„•} [NeZero d] (hd : 2 ≀ d) {g : ℝ} (hg : g ∈ Set.Ico 0 1) {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {E : BlockMat d} {Ξ¨ : ℝ β†’ ℝ} {K : ℝ} {S : CoeffSpace d β†’ ℝ} (hdag : CoarseEllipticityDagger P g E Ξ¨ K S) {Cd : ℝ} (hCd : max 1 (12 * ↑d * βˆšβ†‘d) ≀ Cd) {l : β„€} (hl : ↑(kZero d) ≀ l) {mAl : Mat d} (hmAl : Matrix.PosDef mAl) {sK : β„€} (hsK : growthBar K ≀ 3 ^ sK) {G : β„•} (hqnorm : β€–roundedGrid l mAlβ€– * βˆšβ†‘d ≀ 3 ^ G) {n : β„€} (hDelta : 0 ≀ n + ↑G - 1 - sK) :
    1 ≀ gridReferenceRatio Cd g K E mAl G ∧ blockSize E (adaptedMean P (roundedGrid l mAl) n) ≀ gridReferenceRatio Cd g K E mAl G

    The absorbed size of the reference against the adapted mean of a rounded selection grid is bounded by the grid reference ratio, uniformly in the generation past the source burn.

    source
    noncomputable def HCPolySupport.HighContrast.Quenched.reverseAdapterFactor {d : β„•} (Cd g K : ℝ) (E : BlockMat d) (mAl : Mat d) (G : β„•) :
    ℝ

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.HighContrast.Quenched.exists_reverse_adapter_error_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 β†’ βˆ€ (l : β„€), ↑(kZero d) ≀ l β†’ βˆ€ (mAl : Mat d), Matrix.PosDef mAl β†’ βˆ€ (G : β„•), β€–roundedGrid l mAlβ€– * βˆšβ†‘d ≀ 3 ^ G β†’ βˆ€ (k n m : β„€), 0 ≀ k β†’ k < n β†’ n < m β†’ l ≀ n β†’ 0 ≀ n + ↑G - 1 - sK β†’ βˆƒ (c : ℝ), 0 ≀ c ∧ BlockMatLoewnerLE (blockSub (annealedBlock P (centeredCube d m)) (adaptedMean P (roundedGrid l mAl) n)) (blockScale c E) ∧ c * blockSize E (adaptedMean P (roundedGrid l mAl) n) ≀ CB * reverseAdapterFactor Cd g K E mAl G * 3 ^ (-(↑m - ↑n))

      The reverse Euclidean adapter with a decaying absorbed size. At every admissible triple of scales the reverse comparison holds with a coefficient whose absorbed size against the adapted mean is bounded by a generation-free law factor times 3^{βˆ’(mβˆ’n)}.