High-contrast homogenization: Provider.Quenched.SmallContrastIsotropyPack

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

The isotropy discharge pack

exists_one_step_family_of_block_var_at_level_conv_family_split is Π-free but takes six hypotheses at the abstract block. This file produces the four with content from their near-reference producers; the remaining two are hFeq, which is rfl at isotropyReference, and hcDeep, which is the scale threshold.

Everything here turns on one scale: the split point

k₀ = kEnt + tiltGap Cd g (cEnt/2) nu (Gacc+1)

where the entry depth is past euclideanEntryThreshold K (cEnt/2) sK. Above k₀ the near-reference comparison's adaptedMean_near_reference applies at every scale and every cell, at the dimension-only constant nearIdentityDefect cEnt sigma. Both thresholds are ⌈log₃ ·⌉-shaped — euclideanEntryThreshold logarithmic in the source gauge and tiltGap logarithmic in boundaryConst · 3^{gG} — so k₀ costs a delay logarithmic in the law parameters, which is precisely what's three_mul_max_one_le_rpow converts into a law-free exponent.

The two thresholds are at least one step

theorem HCPolySupport.HighContrast.Quenched.add_one_le_euclideanEntryThreshold (K cEnt : ℝ) (sK : ℤ) : sK + 1 ≤ euclideanEntryThreshold K cEnt sK

theorem HCPolySupport.HighContrast.Quenched.one_le_tiltGap {d : ℕ} (Cd g cEnt : ℝ) (m : Mat d) (G : ℕ) : 1 ≤ tiltGap Cd g cEnt m G

noncomputable def HCPolySupport.HighContrast.Quenched.isotropySplit {d : ℕ} (K cEnt Cd g : ℝ) (nu : Mat d) (G : ℕ) (sK : ℤ) : ℤ

The split point. Past it, the near-reference comparison's comparison holds at every scale.

Equations

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

theorem HCPolySupport.HighContrast.Quenched.le_isotropySplit {d : ℕ} (K cEnt Cd g : ℝ) (nu : Mat d) (G : ℕ) (sK : ℤ) : sK + 2 ≤ isotropySplit K cEnt Cd g nu G sK

The four members with content

theorem HCPolySupport.HighContrast.Quenched.hiso_of_isotropySplit {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) (hstat : IsStationaryLaw P) {l : ℤ} (hl : ↑(kZero d) ≤ l) {Cd : ℝ} (hCd : max 1 (12 * ↑d * √↑d) ≤ Cd) {nu : Mat d} (hnu : Matrix.PosDef nu) {Gacc : ℕ} (hqnorm : ‖roundedGrid l nu‖ * √↑d ≤ 3 ^ Gacc) {sK : ℤ} (hsK : growthBar K ≤ 3 ^ sK) {sigma cEnt : ℝ} (hsigma : refContrast E - 1 ≤ sigma) (hsigma0 : 0 ≤ sigma) (hcEnt : 0 < cEnt) (hkEnt0 : 0 ≤ euclideanEntryThreshold K (cEnt / 2) sK) (hlsplit : l ≤ isotropySplit K (cEnt / 2) Cd g nu (Gacc + 1) sK) (hentry0 : sourceMomentTwo K ≤ 3 ^ (isotropySplit K (cEnt / 2) Cd g nu (Gacc + 1) sK + ↑(Gacc + 1) - sK)) (k : ℤ) : isotropySplit K (cEnt / 2) Cd g nu (Gacc + 1) sK ≤ k → ∀ (w : Fin d → ℤ), BlockMatLoewnerLE (annealedBlock P (adaptedCellAt (roundedGrid l nu) k w)) (blockScale (1 + nearIdentityDefect cEnt sigma) E)

Member 1: the isotropy family the split row cap consumes. Above the split point every aligned cell's annealed block sits below (1+cIso)𝐄.

theorem HCPolySupport.HighContrast.Quenched.isotropy_carriers_of_isotropySplit {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) (hstat : IsStationaryLaw P) {l : ℤ} (hl : ↑(kZero d) ≤ l) {Cd : ℝ} (hCd : max 1 (12 * ↑d * √↑d) ≤ Cd) {nu : Mat d} (hnu : Matrix.PosDef nu) {Gacc : ℕ} (hqnorm : ‖roundedGrid l nu‖ * √↑d ≤ 3 ^ Gacc) {sK : ℤ} (hsK : growthBar K ≤ 3 ^ sK) {sigma cEnt : ℝ} (hsigma : refContrast E - 1 ≤ sigma) (hsigma0 : 0 ≤ sigma) (hcEnt : 0 < cEnt) (hsmall : nearIdentityDefect cEnt sigma < 1) (hkEnt0 : 0 ≤ euclideanEntryThreshold K (cEnt / 2) sK) (hentry0 : sourceMomentTwo K ≤ 3 ^ (isotropySplit K (cEnt / 2) Cd g nu (Gacc + 1) sK + ↑(Gacc + 1) - sK)) (r : ℤ) : isotropySplit K (cEnt / 2) Cd g nu (Gacc + 1) sK ≤ r → BlockMatLoewnerLE (adaptedMean P (roundedGrid l nu) r) (isotropyReference (nearIdentityDefect cEnt sigma) E) ∧ BlockMatLoewnerLE E (blockScale (isotropyKap2 (nearIdentityDefect cEnt sigma)) (adaptedMean P (roundedGrid l nu) r))

Members 2 and 3: the envelope and the comparability. Above the split point the adapted mean is within (1 ± cIso) of the reference, so it sits below isotropyReference cIso 𝐄 and dominates 𝐄 at isotropyKap2 cIso.

Member 4: the maximal envelope at the isotropy block