High-contrast homogenization: Entry.Multiscale.Global.PotentialDecreases #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The partial-change and failed-test potential decreases #
The remaining two of the four potential decreases of the printed proof — the partial geometry
change and the failed comparison test — together with the initial value of the potential. They
serve e.global.selection.partial.change and e.global.selection.failed.test.
theorem
HCPolySupport.HighContrast.Multiscale.partial_change_decrease
{d : ℕ}
(P : MeasureTheory.Measure (CoeffSpace d))
(γ : ℝ)
(jStar : ℕ)
(η a c C Q ε δ : ℝ)
(m mP : Mat d)
(k n : ℤ)
(L h : ℕ)
(hd : 0 < d)
(hη : η ∈ Set.Ioc 0 1)
(hC : 1 ≤ C)
(hCd : ↑d ≤ C)
(hQ : 0 ≤ Q)
(hh : 1 ≤ h)
(ha1 : 1 ≤ a)
(ha : 4 * Q * max 1 C ≤ a * C / ↑d)
(_hδ : 0 ≤ δ)
(_hε : 0 < ε)
(hcomp : 1 / 2 * Real.log ((1 + δ) / (1 - δ)) + 2 * C * (↑h + 2) * Real.log (1 + δ) ≤ ε / 2)
(hw : Real.log (1 + C * ↑h) + c ≤ a * ε / 2)
(hmet :
projectiveDistance mP (explicitCanonicalMetric (adaptedMean P (Geometry.explicitRoundedGrid jStar mP) (n + ↑L))) - projectiveDistance m (explicitCanonicalMetric (adaptedMean P (Geometry.explicitRoundedGrid jStar m) k)) ≤ -ε + 1 / 2 * detIncrement P (Geometry.explicitRoundedGrid jStar m) k (n + 2 * ↑L) + 1 / 2 * Real.log ((1 + δ) / (1 - δ)))
(hx0 :
0 ≤ profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n)
(hxP0 :
0 ≤ profile P γ (Geometry.explicitRoundedGrid jStar mP) jStar (n + ↑L) (n + ↑L) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar mP) jStar (n + ↑L))
(hxP1 :
profile P γ (Geometry.explicitRoundedGrid jStar mP) jStar (n + ↑L) (n + ↑L) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar mP) jStar (n + ↑L) ≤ 1)
(hx'0 :
0 ≤ profile P γ (Geometry.explicitRoundedGrid jStar mP) jStar (n + ↑L) (n + ↑L + ↑h) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar mP) jStar (n + ↑L + ↑h))
(hΔ : 0 ≤ detIncrement P (Geometry.explicitRoundedGrid jStar m) k (n + 2 * ↑L))
(hΔ' : 0 ≤ detIncrement P (Geometry.explicitRoundedGrid jStar mP) (n + ↑L) (n + ↑L + ↑h))
(hspan :
profile P γ (Geometry.explicitRoundedGrid jStar mP) jStar (n + ↑L) (n + ↑L + ↑h) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar mP) jStar (n + ↑L + ↑h) ≤ C * ↑h * (profile P γ (Geometry.explicitRoundedGrid jStar mP) jStar (n + ↑L) (n + ↑L) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar mP) jStar (n + ↑L) + (Real.exp (Q * detIncrement P (Geometry.explicitRoundedGrid jStar mP) (n + ↑L) (n + ↑L + ↑h)) - 1)))
:
e.global.selection.partial.change, scalar assembly: metric part as in
partial_change_metric (premise hmet), profile part by scalar_span with ℓ = h, constants
by comparison_choice (first branch) and weight_choice.
theorem
HCPolySupport.HighContrast.Multiscale.failed_test_decrease
{d : ℕ}
(P : MeasureTheory.Measure (CoeffSpace d))
(γ : ℝ)
(jStar : ℕ)
(η a c C Q ε σ δ : ℝ)
(m mP : Mat d)
(k n : ℤ)
(L H h : ℕ)
(hd : 0 < d)
(hη : η ∈ Set.Ioc 0 1)
(hC : 1 ≤ C)
(hQ : 0 ≤ Q)
(hH : 1 ≤ H)
(ha1 : 1 ≤ a)
(ha : 4 * Q * max 1 C ≤ a * C / ↑d)
(hδ : 0 ≤ δ)
(hε : ε ∈ Set.Ioc 0 1)
(hσ : 0 < σ)
(hc : 0 ≤ c)
(hlogL : 0 ≤ Real.log (1 + 2 * C * ↑L))
(hcomp : 1 / 2 * Real.log ((1 + δ) / (1 - δ)) + 2 * C * (↑h + 2) * Real.log (1 + δ) ≤ C * σ / 4)
(hw : 4 * (Real.log (1 + 2 * C * ↑L) + Real.log (1 + C * ↑H) + c) ≤ a * C * ε * σ)
(hmet :
projectiveDistance mP (explicitCanonicalMetric (adaptedMean P (Geometry.explicitRoundedGrid jStar mP) (n + ↑L))) ≤ 1 / 2 * Real.log ((1 + δ) / (1 - δ)))
(hold : 0 ≤ projectiveDistance m (explicitCanonicalMetric (adaptedMean P (Geometry.explicitRoundedGrid jStar m) k)))
(hx0 :
0 ≤ profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n)
(hxP0 :
0 ≤ profile P γ (Geometry.explicitRoundedGrid jStar mP) jStar (n + ↑L) (n + ↑L) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar mP) jStar (n + ↑L))
(hxP1 :
profile P γ (Geometry.explicitRoundedGrid jStar mP) jStar (n + ↑L) (n + ↑L) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar mP) jStar (n + ↑L) ≤ 1)
(hx'0 :
0 ≤ profile P γ (Geometry.explicitRoundedGrid jStar mP) jStar (n + ↑L) (n + ↑L + ↑H) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar mP) jStar (n + ↑L + ↑H))
(hΔ' : ↑d * σ ≤ detIncrement P (Geometry.explicitRoundedGrid jStar mP) (n + ↑L) (n + ↑L + ↑H))
(hspan :
profile P γ (Geometry.explicitRoundedGrid jStar mP) jStar (n + ↑L) (n + ↑L + ↑H) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar mP) jStar (n + ↑L + ↑H) ≤ C * ↑H * (profile P γ (Geometry.explicitRoundedGrid jStar mP) jStar (n + ↑L) (n + ↑L) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar mP) jStar (n + ↑L) + (Real.exp (Q * detIncrement P (Geometry.explicitRoundedGrid jStar mP) (n + ↑L) (n + ↑L + ↑H)) - 1)))
:
e.global.selection.failed.test, scalar assembly: the candidate was reached
(m₊ = m⋆), so the new metric term is ≤ ½ log((1+δ)/(1-δ)) by the bridge sandwich; profile
by scalar_span with ℓ = H; the failed test Δ' ≥ dσ absorbs the constants in quarters.