High-contrast homogenization: Entry.TwoGridTransport

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

Two-grid transport

The literal polynomial-entry-level form of the paper's Proposition p.two.grid.transport: for each dimension d ≥ 2 and each γ ∈ [0,1) there are constants C(d,γ) ≥ 1 and C_src(d,γ) > 0 such that, whenever two rounded grids of positive-definite metrics are within projective distance one and their annealed blocks are Loewner-close up to δ, the terminal profile plus determinant drift of the transported geometry obeys the printed bound C(δ + ρ). The declaration two_grid_transport is the paper's Proposition p.two.grid.transport, matching the printed statement.

theorem HCPolySupport.HighContrast.Entry.two_grid_transport (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ ρ ∈ Set.Ioc 0 1, ∀ δ ∈ Set.Icc 0 (1 / 4), ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K S → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (m mPlus : Mat d), Matrix.PosDef m → Matrix.PosDef mPlus → ∀ (k n : ℤ), ↑jStar ≤ k → k ≤ n → ∀ (L : ℕ), adaptedCell (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑L) ∪ adaptedCell (Geometry.explicitRoundedGrid jStar mPlus) (n + ↑L) ⊆ centeredCube d (2 * ↑jStar) → C * (↑L + Real.logb 3 ((2 + aspectRatio E) * (‖m‖ * ‖m⁻¹‖))) ≤ ↑n - ↑jStar → projectiveDistance m mPlus ≤ 1 → C + Real.logb 3 ρ⁻¹ ≤ ↑L → profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k (n + 2 * ↑L) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar (n + 2 * ↑L) ≤ 3 ^ (-(1 / 2) * (1 - γ) * ↑L) * ρ → BlockMatLoewnerLE (blockScale (1 - δ) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑L))) (adaptedMean P (Geometry.explicitRoundedGrid jStar mPlus) (n + ↑L)) → BlockMatLoewnerLE (adaptedMean P (Geometry.explicitRoundedGrid jStar mPlus) (n + ↑L)) (blockScale (1 + δ) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑L))) → profile P γ (Geometry.explicitRoundedGrid jStar mPlus) jStar (n + ↑L) (n + ↑L) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar mPlus) jStar (n + ↑L) ≤ C * (δ + ρ)

The literal two-grid transport type, assembled from the ordinary endpoint.