High-contrast homogenization: Entry.Annealed.TwoGridTransport

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

Two Grid Transport

The endpoint length and decay estimates of the two-grid transport, and the transport estimate itself on the rounded grid. The length premise L ≥ C + log₃(ρ⁻¹) gives 1 ≤ L and the endpoint decay 3^{-L} ≤ ρ; the two terms of the smallness premise are weighted against that decay, the linear factor 1 + 2x is absorbed by a positive exponential, and ordered source constants absorb both printed source terms. On two positive definite geometries within projective distance one and Loewner-close annealed blocks, the terminal profile plus determinant drift of the transported geometry then obeys the printed bound C(δ + ρ). These estimates serve Proposition p.two.grid.transport.

theorem HCPolySupport.HighContrast.Annealed.transport_length_decay (C ρ : ℝ) (hC : 1 ≤ C) (hρ : ρ ∈ Set.Ioc 0 1) (L : ℕ) (hL : C + Real.logb 3 ρ⁻¹ ≤ ↑L) : 1 ≤ L ∧ 3 ^ (-↑L) ≤ ρ

The length premise supplies the missing positive length and the final decay.

theorem HCPolySupport.HighContrast.Annealed.transport_weighted_smallness (γ p D ρ L : ℝ) (hγ : γ < 1) (hL : 0 ≤ L) (hp : 0 ≤ p) (hD : 0 ≤ D) (hsmall : p + D ≤ 3 ^ (-(1 / 2) * (1 - γ) * L) * ρ) : 3 ^ ((1 - γ) / 2 * L) * p + 3 ^ ((1 - γ) / 4 * L) * D ≤ ρ ∧ 3 ^ ((1 - γ) / 2 * L) * p ≤ ρ ∧ 3 ^ ((1 - γ) / 4 * L) * D ≤ ρ

Nonnegativity permits weighting the two terms of the smallness premise.

theorem HCPolySupport.HighContrast.Annealed.transport_linear_rpow_bound (b x : ℝ) (hb : 0 < b) (hx : 0 ≤ x) : (1 + 2 * x) * 3 ^ (-b * x) ≤ 1 + 2 / (b * Real.log 3)

A linear factor is uniformly bounded by a positive exponential.

theorem HCPolySupport.HighContrast.Annealed.exists_transport_source_absorption (a Q : ℝ) (ha : 0 < a) (hQ : 0 ≤ Q) : ∃ (Csep : ℝ) (Cpoly : ℝ), 1 ≤ Csep ∧ 0 < Cpoly ∧ ∀ (A L x : ℝ), 1 ≤ A → 0 ≤ L → Csep * (L + Real.logb 3 A) ≤ x → A ^ Q * 3 ^ (-(2 * a) * x) ≤ 3 ^ (-L) ∧ A * (1 + x + L) * 3 ^ (-a * x) ≤ Cpoly * 3 ^ (-L)

Ordered source constants absorb both printed source terms, including the linear scale factor.

theorem HCPolySupport.HighContrast.Annealed.transport_source_brackets (K₀ : ℝ) (hK₀ : 1 ≤ K₀) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ (Pi e ePlus : ℝ), 1 ≤ Pi → 1 ≤ e → 0 ≤ ePlus → ePlus ≤ Real.exp 1 * e → 1 + Pi * (K₀ * e * ePlus + ePlus ^ 2) ≤ B * ((2 + Pi) * e ^ 2) ∧ 1 + Pi * (e + ePlus) ^ 2 ≤ B * ((2 + Pi) * e ^ 2)

Projective proximity bounds the two distinct source brackets by one geometric base.

theorem HCPolySupport.HighContrast.Annealed.two_grid_transport_roundedGrid (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)) [MeasureTheory.IsProbabilityMeasure P] (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), 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 * (δ + ρ)

Transport of the complete profile with the single printed constant.