High-contrast homogenization: Entry.Multiscale.Global.RunState #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The finite run of p.scale.selection: the state and the entry/initialization lemmas #
This file carries the continuing datum of the run that closes global_run
(p.global.selection) and the three landed lemmas that do not mention a step:
RunStateis the continuing datum(𝔪_i, k_i, n_i)together with the invariants that every application ofSelectionData.Selectsneeds at entry: positivity of the metric,j_* ≤ k < n, the eccentricity clausee.renormalization.eccentricity.output, the two entry implicationsk = n → 𝒫 + D ≤ 1andk < n → k + h ≤ n, and the two run fields the tail clauses do not re-establish — the accumulated projective displacementd_pr(Id, 𝔪_i) ≤ ε(i+1)and the generation budgetn_i ≤ n₀ + (2L+H+h)(i+1). Those last two buy the containment premise at stepi+1(R1).runGaugeis the transferred Lyapunov functionΦ_tilde = Φ + w·Rofrun_energy_transfer: the determinant charges are paid out of the reserverun_reserveas they are made, soexists_stop_of_potentialis applied withcharge ≡ 0andBud = 0, and the paper's budgetΦ₁ + aC(h+2)log(24Π)appears as the initial boundR4+R5.run_entry_containment(R1),run_initial(R4) andrun_initial_reserve(R5) are landed with complete proofs (standard axioms only).
The steps are in HCPoly.Entry.Multiscale.Global.RunSteps and
HCPoly.Entry.Multiscale.Global.RunStepsChange, the stop and the stopping argument in
HCPoly.Entry.Multiscale.Global.RunStop, and the assembly with the two Selects projections in
HCPoly.Entry.Multiscale.Global.RunAssembly.
§1 The run state #
The continuing datum of the run (p.global.selection) together with the entry
invariants of SelectionData.Selects. i is the step index; n₀ is the entry generation
of initial_provider_input.
- m : Mat d
The retained metric
𝔪_i. - k : ℤ
The retained generation
k_iof the geometry. - n : ℤ
The current generation
n_i. - i : ℕ
The step index
i. - hm : Matrix.PosDef self.m
𝔪_i > 0. j_* ≤ k_i.k_i ≤ n_i.- hecc : 1 / 2 * Real.log (‖self.m‖ * ‖self.m⁻¹‖) ≤ ε / ↑(S.L ε σ) * (↑self.k - ↑jStar - ↑⌈B * Real.logb 3 (2 + aspectRatio E)⌉)
e.renormalization.eccentricity.outputat(𝔪_i, k_i). - hone : self.k = self.n → profile P γ (Geometry.explicitRoundedGrid jStar self.m) jStar self.n self.n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar self.m) jStar self.n ≤ 1
e.renormalization.output, first clause. e.renormalization.output, second clause.Accumulated projective displacement (
p.global.selection).Generation budget (
p.global.selection).
Instances For
The transferred Lyapunov gauge Φ_tilde = Φ + w·R of run_energy_transfer: the potential
plus w times the determinant reserve of the retained grid.
Equations
- One or more equations did not get rendered due to their size.
Instances For
§2 Entry premises of Selects (landed) #
(R1) Entry containment. The containment premise of Selects, for two grids whose
metrics both have eccentricity at most e. Route: explicitRoundedGrid_opNorm_le gives
‖𝒬(𝔪)‖ ≤ 2(‖𝔪‖‖𝔪⁻¹‖)^{1/2} ≤ 2 e^{e}, and adaptedCell_subset_centeredCube_of_opNorm at
ρ := 2 * Real.exp e needs (j:ℝ) + logb 3 (2√d · 2e^{e}) ≤ 2 j_*; since
2√d · 2 = 2√(4d), that is the hypothesis hj (the factor 2 of explicitRoundedGrid_opNorm_le
absorbed by instantiating containment_arith at d := 4d), and
logb 3 (2√(4d) · e^{e}) = logb 3 (2√(4d)) + e / log 3.
§3 Initialization (landed) #
(R4) The initial state and the initial potential
(p.global.selection). initial_provider_input gives n₀ with
𝒫 + D ≤ ηinit = 1 at (Id, n₀, n₀) and d_pr(Id, m(𝐀_{n₀,Id})) ≤ Cgeom log(2+4Π); the
Alt-1 start-up disjunct of Selects at that tuple (hstart) advances to
(Id, n₀, n₀ + h), which is the paper's (𝔪₁, 𝔮₁, k₁, n₁). The potential bound is
scalar_span (ScalarLemmas.lean, ℓ = 1) followed by the arithmetic comparison of
the logarithmic terms supplied by harith, whose premise Δ ≤ Cdet log(2+Π) at n₀ is hdet,
obtained from blockLogDet_le_of_initial_sandwich + refBlock_le_six_aspect applied to the
sandwich hsand₁/hsand₂. The invariants: hm is Matrix.PosDef.one;
hecc is ‖1‖‖1⁻¹‖ = 1 and hn₀; hone is vacuous for 1 ≤ S.h; hgap is rfl-level;
hpr is projectiveDistance_self; hgen is hn₀.
(R5) The charge budget, as the initial reserve bound (p.global.selection).
The determinant charges are transferred into the reserve step by step
(run_energy_transfer), so exists_stop_of_potential runs with charge ≡ 0 and Bud = 0
and the paper's budget Φ₁ + aC(h+2)log(24Π) is exactly
potential ≤ C' log₃(2+Π) (R4) plus this bound on the initial reserve. Route:
run_reserve_initial (with the extra binder hjn₀ : (jStar : ℤ) ≤ n₀) with monotonicity of r ↦ blockLogDet (adaptedMean P (𝒬 Id) r) from
the annealed order, then blockLogDet_le_of_initial_sandwich (whose hsix is
refBlock_le_six_aspect) at the sandwich hsand₁/hsand₂ of initial_provider_input.