High-contrast homogenization: Entry.Multiscale.ScaleSelection.TransportAlternative

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

The transport application and the change-of-geometry alternative

Group D of the printed proof (p.scale.selection), third part: the two-grid transport applied to the updated geometry, and alternative 2 with its output profile bound C σ^{(1-γ)/8}, its output eccentricity and its two output conditions.

Part of the proof of the statement in HCPoly/Entry/Statements/ScaleSelection.lean. Conventions of the entire group: q = 𝒬(𝔪) is Geometry.explicitRoundedGrid jStar m; the printed data are h = 2Q, c = c₀, L(ε,σ) = selectionLength L₀ σ and B₀(ε,σ) = max 1 (max (B₀^bridge (√ε σ) L) (2 C_tr (L+1))); √ε is the printed ε^{1/2}; the source lower scale e.source.lower.scale is carried wherever j_* appears with the law, and no integrability, finiteness or measurability premise is added anywhere. Unused hypothesis binders of a statement are underscore-prefixed; the tree compiles with -DwarningAsError=true.

The declaration text of this file is the closed skeleton's, copied unchanged; only this header, the imports and the namespace frame are new.

theorem HCPolySupport.HighContrast.Multiscale.transport_application (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (Csrc C₁ : ℝ) (hC₁ : 0 < C₁) (hone : OneGridBody d γ Csrc C₁) (Ctr : ℝ) (hCtr : 1 ≤ Ctr) (htr : TransportBody d γ Ctr Csrc) (L₀ : ℕ) (hL₀ : 1 ≤ L₀) (hCtrL₀ : Ctr ≤ ↑L₀) (c₀ : ℝ) (hc₀ : c₀ ∈ Set.Ioo 0 1) (B₀ : ℝ → ℕ → ℝ) (hbr : BridgeBody d γ L₀ c₀ Csrc B₀) (ε₁ : ℝ) (hsmall : ∀ (ε σ : ℝ), ε ∈ Set.Ioc 0 ε₁ → σ ∈ Set.Ioc 0 ε → 2 * C₁ * (1 + 2 * ↑(bigQ d γ) * ↑d) * (1 + ↑(selectionLength L₀ σ)) * ε * σ ≤ 3 ^ (-(1 / 2) * (1 - γ) * ↑(selectionLength L₀ σ)) * σ ^ ((1 - γ) / 8)) (ε σ B : ℝ) (hε4 : ε ∈ Set.Ioc 0 (1 / 4)) (hεc : ε ≤ (c₀ / (↑d + 1)) ^ 2) (hε₁ : ε ≤ ε₁) (hQε : ↑(bigQ d γ) * ↑d * ε ≤ Real.log 2) (hLε : 2 * Ctr * ε ≤ ↑L₀ * Real.log 3) (hσ : σ ∈ Set.Ioc 0 ε) (hB1 : B₀ (√ε * σ) (selectionLength L₀ σ) ≤ B) (hB2 : 2 * Ctr * (↑(selectionLength L₀ σ) + 1) ≤ B) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hP : MeasureTheory.IsProbabilityMeasure P) (hstat : IsStationaryLaw P) (hunit : IsUnitRangeLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (hsrc : ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar) (m : Mat d) (hm : Matrix.PosDef m) (k n : ℤ) (hjk : ↑jStar ≤ k) (hkn : k ≤ n) (hecc : 1 / 2 * Real.log (‖m‖ * ‖m⁻¹‖) ≤ ε / ↑(selectionLength L₀ σ) * (↑k - ↑jStar - ↑⌈B * Real.logb 3 (2 + aspectRatio E)⌉)) (hin2 : k < n → k + ↑(2 * bigQ d γ) ≤ n) (hcont : adaptedCell (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑(selectionLength L₀ σ)) ∪ adaptedCell (Geometry.explicitRoundedGrid jStar (geometryUpdate ε m (explicitCanonicalMetric (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑(selectionLength L₀ σ)))))) (n + ↑(selectionLength L₀ σ)) ⊆ centeredCube d (2 * ↑jStar)) (hk : k < n) (hη : profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n ≤ c₀ * ε * σ) (hlong : (↑d)⁻¹ * detIncrement P (Geometry.explicitRoundedGrid jStar m) n (n + 2 * ↑(selectionLength L₀ σ)) ≤ ε * σ) : profile P γ (Geometry.explicitRoundedGrid jStar (geometryUpdate ε m (explicitCanonicalMetric (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑(selectionLength L₀ σ)))))) jStar (n + ↑(selectionLength L₀ σ)) (n + ↑(selectionLength L₀ σ)) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar (geometryUpdate ε m (explicitCanonicalMetric (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑(selectionLength L₀ σ)))))) jStar (n + ↑(selectionLength L₀ σ)) ≤ Ctr * (√ε * σ + σ ^ ((1 - γ) / 8))

p.scale.selection: the two-grid transport applies with δ = ε^{1/2}σ, ρ = σ^{(1−γ)/8}.

theorem HCPolySupport.HighContrast.Multiscale.transport_alternative (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (Csrc C₁ : ℝ) (hC₁ : 0 < C₁) (hone : OneGridBody d γ Csrc C₁) (Ctr : ℝ) (hCtr : 1 ≤ Ctr) (htr : TransportBody d γ Ctr Csrc) (C : ℝ) (hC : 2 * Ctr ≤ C) (L₀ : ℕ) (hL₀ : 1 ≤ L₀) (hCtrL₀ : Ctr ≤ ↑L₀) (c₀ : ℝ) (hc₀ : c₀ ∈ Set.Ioo 0 1) (B₀ : ℝ → ℕ → ℝ) (hbr : BridgeBody d γ L₀ c₀ Csrc B₀) (ε₁ : ℝ) (hsmall : ∀ (ε σ : ℝ), ε ∈ Set.Ioc 0 ε₁ → σ ∈ Set.Ioc 0 ε → 2 * C₁ * (1 + 2 * ↑(bigQ d γ) * ↑d) * (1 + ↑(selectionLength L₀ σ)) * ε * σ ≤ 3 ^ (-(1 / 2) * (1 - γ) * ↑(selectionLength L₀ σ)) * σ ^ ((1 - γ) / 8)) (ε σ B : ℝ) (hε4 : ε ∈ Set.Ioc 0 (1 / 4)) (hεc : ε ≤ (c₀ / (↑d + 1)) ^ 2) (hε₁ : ε ≤ ε₁) (hQε : ↑(bigQ d γ) * ↑d * ε ≤ Real.log 2) (hCε : C * ε ^ ((1 - γ) / 8) ≤ 1) (hLε : 2 * Ctr * ε ≤ ↑L₀ * Real.log 3) (hσ : σ ∈ Set.Ioc 0 ε) (hB1 : B₀ (√ε * σ) (selectionLength L₀ σ) ≤ B) (hB2 : 2 * Ctr * (↑(selectionLength L₀ σ) + 1) ≤ B) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hP : MeasureTheory.IsProbabilityMeasure P) (hstat : IsStationaryLaw P) (hunit : IsUnitRangeLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (hsrc : ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar) (m : Mat d) (hm : Matrix.PosDef m) (k n : ℤ) (hjk : ↑jStar ≤ k) (hkn : k ≤ n) (hecc : 1 / 2 * Real.log (‖m‖ * ‖m⁻¹‖) ≤ ε / ↑(selectionLength L₀ σ) * (↑k - ↑jStar - ↑⌈B * Real.logb 3 (2 + aspectRatio E)⌉)) (hin2 : k < n → k + ↑(2 * bigQ d γ) ≤ n) (hcont : adaptedCell (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑(selectionLength L₀ σ)) ∪ adaptedCell (Geometry.explicitRoundedGrid jStar (geometryUpdate ε m (explicitCanonicalMetric (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑(selectionLength L₀ σ)))))) (n + ↑(selectionLength L₀ σ)) ⊆ centeredCube d (2 * ↑jStar)) (hk : k < n) (hη : profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n ≤ c₀ * ε * σ) (hlong : (↑d)⁻¹ * detIncrement P (Geometry.explicitRoundedGrid jStar m) n (n + 2 * ↑(selectionLength L₀ σ)) ≤ ε * σ) : (k < n ∧ profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n ≤ c₀ * ε * σ ∧ (↑d)⁻¹ * detIncrement P (Geometry.explicitRoundedGrid jStar m) n (n + 2 * ↑(selectionLength L₀ σ)) ≤ ε * σ ∧ profile P γ (Geometry.explicitRoundedGrid jStar (geometryUpdate ε m (explicitCanonicalMetric (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑(selectionLength L₀ σ)))))) jStar (n + ↑(selectionLength L₀ σ)) (n + ↑(selectionLength L₀ σ)) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar (geometryUpdate ε m (explicitCanonicalMetric (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑(selectionLength L₀ σ)))))) jStar (n + ↑(selectionLength L₀ σ)) ≤ C * σ ^ ((1 - γ) / 8)) ∧ 1 / 2 * Real.log (‖geometryUpdate ε m (explicitCanonicalMetric (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑(selectionLength L₀ σ))))‖ * ‖(geometryUpdate ε m (explicitCanonicalMetric (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑(selectionLength L₀ σ)))))⁻¹‖) ≤ ε / ↑(selectionLength L₀ σ) * (↑n + ↑(selectionLength L₀ σ) - ↑jStar - ↑⌈B * Real.logb 3 (2 + aspectRatio E)⌉) ∧ (n + ↑(selectionLength L₀ σ) = n + ↑(selectionLength L₀ σ) → profile P γ (Geometry.explicitRoundedGrid jStar (geometryUpdate ε m (explicitCanonicalMetric (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑(selectionLength L₀ σ)))))) jStar (n + ↑(selectionLength L₀ σ)) (n + ↑(selectionLength L₀ σ)) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar (geometryUpdate ε m (explicitCanonicalMetric (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑(selectionLength L₀ σ)))))) jStar (n + ↑(selectionLength L₀ σ)) ≤ 1) ∧ (n + ↑(selectionLength L₀ σ) < n + ↑(selectionLength L₀ σ) → n + ↑(selectionLength L₀ σ) + ↑(2 * bigQ d γ) ≤ n + ↑(selectionLength L₀ σ))

Alternative 2, change of geometry (p.scale.selection): the transport output ≤ Cσ^{(1−γ)/8} ≤ 1, the output eccentricity from l.projective.step, and the vacuous clause.