High-contrast homogenization: Entry.SuccessfulShortBridge #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The successful short bridge #
The exact type of p.successful.short.bridge.
All ordinary analytic obligations are discharged in Annealed.ShortBridge.
The probability proof is introduced at its position and then installed
as an instance. Unit-range is forwarded in its original position; the ordinary
mathematical proof does not use it.
theorem
HCPolySupport.HighContrast.Entry.successful_short_bridge
(d : ℕ)
(hd : 2 ≤ d)
(γ : ℝ)
(hγ : γ ∈ Set.Ico 0 1)
:
∃ (L₀ : ℕ),
∃ c₀ ∈ Set.Ioo 0 1,
∃ (Csrc : ℝ),
0 < Csrc ∧ ∀ σ ∈ Set.Ioc 0 1,
∀ (L : ℕ),
↑L₀ + ⌈Real.logb 3 σ⁻¹⌉ ≤ ↑L →
∃ (B₀ : ℝ),
1 ≤ B₀ ∧ ∀ (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 →
adaptedCell (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑L) ∪ adaptedCell (Geometry.explicitRoundedGrid jStar mPlus) (n + ↑L) ⊆
centeredCube d (2 * ↑jStar) →
Real.log (‖m‖ * ‖m⁻¹‖) ≤ c₀ / ↑L * (↑k - ↑jStar - ↑⌈B₀ * Real.logb 3 (2 + aspectRatio E)⌉) →
k + 2 * ↑(bigQ d γ) ≤ n →
projectiveDistance m mPlus ≤ 1 →
profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ
(Geometry.explicitRoundedGrid jStar m) jStar n + detIncrement P (Geometry.explicitRoundedGrid jStar m) n
(n + 2 * ↑L) ≤ c₀ * σ →
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)))
The short-bridge type, assembled from the ordinary rounded-grid theorem.