High-contrast homogenization: Entry.Multiscale.Global.Run

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

EccentricityScaleDecay lemmas for global_run

This file collects the sixteen run_* helper lemmas behind global_run — the reserve, potential and service-decrease machinery — and the quarter-step potential-decrease lemma potential_step_sub_le_of_quarter_bound. It also proves four small lemmas the assembly needs: a weight_choice variant whose witness also dominates d, an upper bound S.eta ε σ ≤ 1 on the selection step, and two algebraic bridges between the (d:ℝ)⁻¹ * Δ test form and the d * ε * σ / d * σ form. This is the per-step machinery of p.global.selection, and through it part of the assembly of t.polynomial.entry.

§1 The sixteen run_* lemmas

theorem HCPolySupport.HighContrast.Multiscale.run_blockLogDet_adaptedMean_nonneg {d : ℕ} (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ) (hP : MeasureTheory.IsProbabilityMeasure P) (hst : IsStationaryLaw P) (_hur : IsUnitRangeLaw P) (hce : CoarseEllipticityDagger P γ E Ψ K Src) (jStar : ℕ) (hjStar : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (j : ℤ) : 0 ≤ blockLogDet (adaptedMean P (Geometry.explicitRoundedGrid jStar m) j)

The adapted mean at a rounded grid has nonnegative block log-determinant.

theorem HCPolySupport.HighContrast.Multiscale.run_adaptedMean_blockPosDef {d : ℕ} (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ) (hP : MeasureTheory.IsProbabilityMeasure P) (hst : IsStationaryLaw P) (hce : CoarseEllipticityDagger P γ E Ψ K Src) (jStar : ℕ) (hjStar : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (j : ℤ) : Book.Ch02.BlockPosDef (adaptedMean P (Geometry.explicitRoundedGrid jStar m) j)

The adapted mean at a rounded grid is block positive-definite.

theorem HCPolySupport.HighContrast.Multiscale.run_output_profile (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ (Cout : ℝ), 0 < Cout → ∀ (H : ℕ), 1 ≤ H → ∃ (Cprof : ℝ), 0 < Cprof ∧ ∀ σ ∈ Set.Ioc 0 1, ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (m : Mat d), Matrix.PosDef m → ∀ (s : ℤ), ↑jStar ≤ s → profile P γ (Geometry.explicitRoundedGrid jStar m) jStar s s + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar s ≤ Cout * σ ^ ((1 - γ) / 8) → profile P γ (Geometry.explicitRoundedGrid jStar m) jStar s s + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar s ≤ 1 → (↑d)⁻¹ * detIncrement P (Geometry.explicitRoundedGrid jStar m) s (s + ↑H) < σ → max (max (profile P γ (Geometry.explicitRoundedGrid jStar m) jStar s s) (profile P γ (Geometry.explicitRoundedGrid jStar m) jStar s (s + ↑H))) (profile P γ (Geometry.explicitRoundedGrid jStar m) jStar (s + ↑H) (s + ↑H)) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar s + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar (s + ↑H) ≤ Cprof * σ ^ ((1 - γ) / 8)

The selected output profile bound, with the source and profile constants furnished before H and σ are fixed.

def HCPolySupport.HighContrast.Multiscale.runReserve (D : ℤ → ℝ) (h : ℕ) (k n : ℤ) : ℝ

The determinant reserve: the sum of h trailing generations plus the current and initial generations.

Equations

• HCPolySupport.HighContrast.Multiscale.runReserve D h k n = ∑ i ∈ Finset.range h, D (n - ↑i) + D n + D k

theorem HCPolySupport.HighContrast.Multiscale.run_reserve_sync {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q : Mat d) (h : ℕ) (k n : ℤ) : runReserve (fun (r : ℤ) => blockLogDet (adaptedMean P q r)) h k n - runReserve (fun (r : ℤ) => blockLogDet (adaptedMean P q r)) h k (n + ↑h) = synchCharge P q (↑h) n + detIncrement P q n (n + ↑h)

The reserve's drop across one h-step matches the synchronized plus one-step loss.

theorem HCPolySupport.HighContrast.Multiscale.run_reserve_nonneg (D : ℤ → ℝ) (h : ℕ) (k n : ℤ) (hD : ∀ (r : ℤ), 0 ≤ D r) : 0 ≤ runReserve D h k n

The reserve is nonnegative when D is.

theorem HCPolySupport.HighContrast.Multiscale.run_reserve_advance (D : ℤ → ℝ) (h : ℕ) (j k n t : ℤ) (hmono : ∀ (r s : ℤ), j ≤ r → r ≤ s → D s ≤ D r) (_hjn : j ≤ n) (hwindow : j + ↑h ≤ n + 1) (hnt : n ≤ t) : D n - D t ≤ runReserve D h k n - runReserve D h k t

The reserve's drop over an advancing window bounds D's drop.

theorem HCPolySupport.HighContrast.Multiscale.run_reserve_change (D D' : ℤ → ℝ) (h : ℕ) (j k n u s t : ℤ) (Λ : ℝ) (hmono : ∀ (r r' : ℤ), j ≤ r → r ≤ r' → D r' ≤ D r) (hmono' : ∀ (r r' : ℤ), j ≤ r → r ≤ r' → D' r' ≤ D' r) (hjn : j ≤ n) (hwindow : j + ↑h ≤ n + 1) (hnu : n ≤ u) (hjs : j ≤ s) (hst : s + ↑h ≤ t) (hjump : D' s ≤ D u + Λ) : D k - D u + (D' s - D' t) - (↑h + 2) * Λ ≤ runReserve D h k n - runReserve D' h s t

The reserve's change across a geometry change, up to a (h+2)Λ jump term.

theorem HCPolySupport.HighContrast.Multiscale.run_reserve_initial (D : ℤ → ℝ) (h : ℕ) (k : ℤ) (hmono : ∀ (r : ℤ), k ≤ r → D r ≤ D k) : runReserve D h k (k + ↑h) ≤ (↑h + 2) * D k

The reserve at the initial generation is bounded by (h+2) D k.

theorem HCPolySupport.HighContrast.Multiscale.run_potential_nonneg {d : ℕ} (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (_hγ : γ ∈ Set.Ico 0 1) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ) (hP : MeasureTheory.IsProbabilityMeasure P) (hst : IsStationaryLaw P) (_hur : IsUnitRangeLaw P) (hce : CoarseEllipticityDagger P γ E Ψ K Src) (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (k n : ℤ) (hk : ↑jStar ≤ k) (hkn : k ≤ n) (η a : ℝ) (hη : 0 < η) (ha : 0 ≤ a) : 0 ≤ potential P γ jStar η a m k n

The potential is nonnegative on the retained geometry.

theorem HCPolySupport.HighContrast.Multiscale.run_reserve_rounded_nonneg {d : ℕ} (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ) (hP : MeasureTheory.IsProbabilityMeasure P) (hst : IsStationaryLaw P) (hur : IsUnitRangeLaw P) (hce : CoarseEllipticityDagger P γ E Ψ K Src) (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (h : ℕ) (k n : ℤ) : 0 ≤ runReserve (fun (r : ℤ) => blockLogDet (adaptedMean P (Geometry.explicitRoundedGrid jStar m) r)) h k n

The reserve built from the rounded-grid adapted mean is nonnegative.

theorem HCPolySupport.HighContrast.Multiscale.run_energy_transfer (φ φ' R R' c w charge J : ℝ) (hw : 0 ≤ w) (hstep : φ' - φ ≤ -c - w * J + w * charge) (hreserve : charge - J ≤ R - R') : φ' + w * R' - (φ + w * R) ≤ -c

Transferring a charge against the reserve preserves the potential-plus-reserve decrease.

§2 The quarter-step potential decrease

theorem HCPolySupport.HighContrast.Multiscale.potential_step_sub_le_of_quarter_bound {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (jStar : ℕ) (η a c C : ℝ) (m : Mat d) (k n : ℤ) (h : ℕ) (hd : 0 < d) (hη : 0 < η) (hC : 1 ≤ C) (ha : ↑d ≤ a) (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 / 4 * (profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n) + C * synchCharge P (Geometry.explicitRoundedGrid jStar m) (↑h) n) : 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

Local variant of potential_step_sub_le_of_exp_bound matching the premise that SelectionData.Selects supplies in its Alternative-1 service disjunct (SelectionData.lean): x' ≤ 1/4 * x + C * Δ̂_h(n). Conclusion is the SAME shape as potential_step_sub_le_of_exp_bound's, so it plugs into exists_stop_of_potential with the same c and the same charge. Needs d ≤ a (the weight already satisfies 4 Q max 1 C ≤ a C / d; d ≤ a is an extra, freely enforceable requirement on weight_choice's a). No Q and no growth bound are needed.

§3 Four new lemmas

theorem HCPolySupport.HighContrast.Multiscale.weight_choice_ge_d (d : ℕ) (hd : 0 < d) (C Q ε σ c L H h : ℝ) (hC : 0 < C) (hε : 0 < ε) (hσ : 0 < σ) : ∃ (a : ℝ), 1 ≤ a ∧ ↑d ≤ a ∧ 4 * Q * max 1 C ≤ a * C / ↑d ∧ Real.log (1 + C * h) + c ≤ a * ε / 2 ∧ 4 * (Real.log (1 + 2 * C * L) + Real.log (1 + C * H) + c) ≤ a * C * ε * σ

weight_choice strengthened so the witness weight also dominates d (as a real number): replace the witness by max a d, using that each of the three conclusions is monotone increasing in a when C, ε, σ > 0.

theorem HCPolySupport.HighContrast.Multiscale.selectionData_eta_le_one (S : SelectionData) (ε σ : ℝ) (hε : ε ∈ Set.Ioc 0 S.eps0) (hσ : σ ∈ Set.Ioc 0 ε) : S.eta ε σ ≤ 1

The selection step η = S.eta ε σ = S.c * ε * σ never exceeds 1, since S.c < 1 and ε, σ ≤ 1.

theorem HCPolySupport.HighContrast.Multiscale.det_bridge_gt (d : ℕ) (hd : 0 < d) (ε σ Δ : ℝ) (h : (↑d)⁻¹ * Δ > ε * σ) : ↑d * ε * σ < Δ

If (d:ℝ)⁻¹ * Δ > ε * σ then d * ε * σ < Δ.

theorem HCPolySupport.HighContrast.Multiscale.det_bridge_not_lt (d : ℕ) (hd : 0 < d) (σ Δ : ℝ) (h : ¬(↑d)⁻¹ * Δ < σ) : ↑d * σ ≤ Δ

If ¬((d:ℝ)⁻¹ * Δ < σ) then d * σ ≤ Δ.