Documentation

LeanPool.HighContrastHomogenization.Entry.Multiscale.Global.Containment

High-contrast homogenization: Entry.Multiscale.Global.Containment #

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

Containment geometry and the first two potential decreases #

p.global.selection: the containment budget — an adapted cell of a grid of controlled operator norm lies in the centred cube □_{2 j_*} — together with the rounded-grid operator-norm bound, the definition of the potential Φ, and the decreases of the h-step and long-step alternatives.

§D Containment geometry (p.global.selection) #

source
theorem HCPolySupport.HighContrast.Multiscale.adaptedCell_subset_centeredCube_of_opNorm {d : ℕ} (q : Mat d) (ρ : ℝ) (j : ℤ) (jStar : ℕ) (hρ : ‖q‖ ≤ ρ) (hρ0 : 0 < ρ) (hj : ↑j + Real.logb 3 (2 * √↑d * ρ) ≤ 2 * ↑jStar) :
adaptedCell q j ⊆ centeredCube d (2 * ↑jStar)

p.global.selection: an adapted cell of a grid with operator norm ≤ ρ at generation j lies in □_{2 jStar} once j + log₃(2 √d ρ) ≤ 2 jStar.

source
theorem HCPolySupport.HighContrast.Multiscale.explicitRoundedGrid_opNorm_le {d : ℕ} (jStar : ℕ) (m : Mat d) (hj : 2 * d ≤ 3 ^ jStar) (hm : Matrix.PosDef m) :
‖Geometry.explicitRoundedGrid jStar m‖ ≤ 2 * (‖m‖ * ‖m⁻¹‖) ^ (1 / 2)

p.global.selection (e.rounded.grid.bounds): ‖𝒬(m)‖ ≤ 2 (‖m‖ ‖m⁻¹‖)^{1/2}; restates Geometry.opNorm_roundedGrid_le with Real.sqrt unfolded to rpow.

§E The potential and its four decreases (e.global.selection.scalar, p.global.selection) #

source
noncomputable def HCPolySupport.HighContrast.Multiscale.potential {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (jStar : ℕ) (η a : ℝ) (m : Mat d) (k n : ℤ) :
ℝ

e.global.selection.scalar: the scalar Φ at the state (m, k, n) on the grid 𝒬(m).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.HighContrast.Multiscale.potential_step_sub_le_of_exp_bound {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (jStar : ℕ) (η a c C Q : ℝ) (m : Mat d) (k n : ℤ) (h : ℕ) (hd : 0 < d) (hη : η ∈ Set.Ioc 0 1) (hC : 1 ≤ C) (hQ : 0 ≤ Q) (ha : 4 * Q * max 1 C ≤ a * C / ↑d) (hc : c = 1 / 2 * η * Real.log (16 / 9)) (hx : η < profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n) (hx' : 0 ≤ profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k (n + ↑h) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar (n + ↑h)) (hΔ : 0 ≤ synchCharge P (Geometry.explicitRoundedGrid jStar m) (↑h) n) (hprop : profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k (n + ↑h) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar (n + ↑h) ≤ 1 / 8 * Real.exp (Q * synchCharge P (Geometry.explicitRoundedGrid jStar m) (↑h) n) * (profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n) + C * (Real.exp (Q * synchCharge P (Geometry.explicitRoundedGrid jStar m) (↑h) n) - 1)) :
    potential P γ jStar η a m k (n + ↑h) - potential P γ jStar η a m k n ≤ -c + a * C / ↑d * synchCharge P (Geometry.explicitRoundedGrid jStar m) (↑h) n

    e.global.selection.h.step: an h-step on a fixed grid with the synchronized propagation output e.fixed.geometry.synchronized.propagation and x > η decreases Φ by c = ½ η log(16/9) up to (aC/d) Δ̂_h(n). Uses scalar_growth_bound, scalar_contraction.

    source
    theorem HCPolySupport.HighContrast.Multiscale.long_step_decrease {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (jStar : ℕ) (η a c C Q ε σ H : ℝ) (m : Mat d) (k n : ℤ) (L : ℕ) (hd : 0 < d) (hη : η ∈ Set.Ioc 0 1) (hC : 1 ≤ C) (hQ : 0 ≤ Q) (hL : 1 ≤ L) (_hc : 0 ≤ c) (hε : 0 < ε) (hσ : 0 < σ) (ha1 : 1 ≤ a) (ha : 4 * Q * max 1 C ≤ a * C / ↑d) (hw : 4 * (Real.log (1 + 2 * C * ↑L) + Real.log (1 + C * H) + c) ≤ a * C * ε * σ) (hlogH : 0 ≤ Real.log (1 + C * H)) (hx0 : 0 ≤ profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n) (hx1 : profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n ≤ 1) (hx'0 : 0 ≤ profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k (n + 2 * ↑L) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar (n + 2 * ↑L)) (hΔ : ↑d * ε * σ < detIncrement P (Geometry.explicitRoundedGrid jStar m) n (n + 2 * ↑L)) (hspan : profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k (n + 2 * ↑L) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar (n + 2 * ↑L) ≤ C * (2 * ↑L) * (profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n + (Real.exp (Q * detIncrement P (Geometry.explicitRoundedGrid jStar m) n (n + 2 * ↑L)) - 1))) :
    potential P γ jStar η a m k (n + 2 * ↑L) - potential P γ jStar η a m k n ≤ -c + a * C / ↑d * detIncrement P (Geometry.explicitRoundedGrid jStar m) n (n + 2 * ↑L)

    e.global.selection.long.step: a 2L obstruction (Δ_{n,n+2L} > dεσ) with the fixed-span output e.fixed.geometry.fixed.span.propagation over 2L generations. Uses scalar_span and the weight choice.