High-contrast homogenization: Entry.Multiscale.PolynomialEntry.Assembly

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

Assembly of t.polynomial.entry

This module assembles the paper's Theorem t.polynomial.entry from the two selection statements p.scale.selection and p.global.selection together with an assumed p.response.transfer. The constants are introduced in the order the paper's proof fixes them, each from the statement that owns it, so that the constant of the conclusion is determined before the coefficient law is quantified over. The bridge from the entry generation to every larger scale is the monotonicity of the annealed contrast in the scale: a contrast bound at the entry generation propagates to all scales above it.

def HCPolySupport.HighContrast.Multiscale.GlobalSelectionBody (d : ℕ) (γ : ℝ) (S : SelectionData) (ε Csrc : ℝ) (H : ℕ) (Cprof σ C : ℝ) : Prop

The conclusion of p.global.selection after its constants ε, Csrc, H, Cprof, σ, C: for every coefficient law satisfying the standing assumptions, every B ≥ B₀(ε,σ), and every generation j_* above the source scale, it produces a symmetric positive block F and two integer scales s < t whose adapted cells, Loewner comparisons, determinant loss and profile drift all satisfy the printed bounds.

Equations

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

def HCPolySupport.HighContrast.Multiscale.ResponseTransferBody (d : ℕ) (γ : ℝ) (S : SelectionData) (ε Csrc : ℝ) (H : ℕ) (Cprof σ Cglob Bresp Cresp δ : ℝ) : Prop

The conclusion of p.response.transfer after its constants Csrc, ε, H, Cprof, σ, Cglob, Bresp, Cresp, δ: given the same coefficient-law data and a symmetric positive block F with scales s < t satisfying the entry hypotheses at a generation above the source scale, it extends the terminal scale to an integer mEnt > t within ⌈Cresp log₃(2+Π)⌉ of t at which the annealed contrast has dropped to 1 + δ.

Equations

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

theorem HCPolySupport.HighContrast.Multiscale.polynomial_entry_of_response_transfer (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (hRT : ∀ (S : SelectionData), S.Selects d γ → ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ ε ∈ Set.Ioc 0 S.eps0, ∀ δ ∈ Set.Ioc 0 1, ∃ (H : ℕ), max 4 S.h ≤ H ∧ ∀ (Cprof : ℝ), 0 < Cprof → ∃ σ₀ ∈ Set.Ioc 0 ε, ∀ σ ∈ Set.Ioc 0 σ₀, ∀ (Cglob : ℝ), 0 < Cglob → ∃ (Bresp : ℝ), 1 ≤ Bresp ∧ ∃ (Cresp : ℝ), 0 < Cresp ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (B : ℝ), max (S.B0 ε σ) Bresp ≤ B → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Cglob * (B + 1) * Real.logb 3 (2 + aspectRatio E) + Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (F : BlockMat d) (s t : ℤ), IsSymmetricBlockMat F → Book.Ch02.BlockPosDef F → s < t → t = s + ↑H → ↑jStar + ⌈B * Real.logb 3 (2 + aspectRatio E)⌉ ≤ s → t ≤ ↑jStar + ⌈(B + Cglob) * Real.logb 3 (2 + aspectRatio E)⌉ → adaptedCell (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) t ⊆ centeredCube d (2 * ↑jStar) → BlockMatLoewnerLE (blockScale (1 - √ε * σ) F) (adaptedMean P (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) s) → BlockMatLoewnerLE (adaptedMean P (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) s) (blockScale (1 + √ε * σ) F) → (↑d)⁻¹ * detIncrement P (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) s t < σ → ⋯ + determinantDrift P γ (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) jStar t ≤ Cprof * σ ^ ((1 - γ) / 8) → ⋯ ≤ (2 + aspectRatio E) ^ Cglob → ∃ (mEnt : ℤ), ⋯) (σ : ℝ) (hσ : σ ∈ Set.Ioc 0 1) : ∃ (C : ℝ), 0 < C ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K S → ∀ (m : ℤ), ⌈C * Real.logb 3 (2 + aspectRatio E * K)⌉ ≤ m → annealedContrast P m ≤ 1 + σ

t.polynomial.entry from p.response.transfer. For every d ≥ 2, every γ ∈ [0,1) and every tolerance σ ∈ (0,1], the conclusion of p.response.transfer — its constants chosen in the printed order after those of p.scale.selection and p.global.selection — implies the polynomial entry estimate: there is a constant C > 0, fixed before the coefficient law is quantified over and depending only on d, γ and σ, such that under the standing assumptions on the law the annealed contrast satisfies Θ_m ≤ 1 + σ at every scale m ≥ ⌈C log₃(2 + Π K)⌉.