High-contrast homogenization: Entry.Multiscale.ScaleSelection.ConsumedBodies

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

The consumed statement bodies and the selection length

The three propositions this decomposition consumes, each written as the body of its statement after the outermost constants (OneGridBody, TransportBody, BridgeBody), and the selection length L = L₀ + ⌈(3/2) log₃ σ⁻¹⌉ of e.bridge.length.choice (p.scale.selection).

Two admitted strengthenings of the printed choices are used, documented here rather than only repeated by formula: L₀ ≥ 1 is obtained by the printed permission to increase L₀, ensuring L > 0; B₀ ≥ 2 C_tr (L+1) is a stronger choice of the statement's own threshold, licensed by p.scale.selection, using log₃(2+Π) ≥ 1/2 from Π ≥ 0. It does not add a hypothesis to Selects.

Part of the proof of HCPoly/Entry/Statements/ScaleSelection.lean. Conventions of the group: q = 𝒬(𝔪) is Geometry.explicitRoundedGrid jStar m; the printed data are h = 2Q, c = c₀, L(ε,σ) = selectionLength L₀ σ and B₀(ε,σ) = max 1 (max (B₀^bridge (√ε σ) L) (2 C_tr (L+1))); √ε is the printed ε^{1/2}; the source lower scale e.source.lower.scale is carried wherever j_* appears with the law, and no integrability, finiteness or measurability premise is added anywhere. Unused hypothesis binders of a statement are underscore-prefixed; the tree compiles with -DwarningAsError=true.

The declaration text of this file is the closed skeleton's, copied unchanged; only this header, the imports and the namespace frame are new.

The consumed statement bodies, after their constants

def HCPolySupport.HighContrast.Multiscale.OneGridBody (d : ℕ) (γ Csrc C : ℝ) : Prop

The body of Entry.fixed_geometry_one_grid_propagation_full (HCPoly/Entry/Statements/OneGridPropagation.lean) after ∃ Csrc, 0 < Csrc ∧ ∃ C, 0 < C ∧, verbatim.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.HighContrast.Multiscale.TransportBody (d : ℕ) (γ C Csrc : ℝ) : Prop

The body of Entry.two_grid_transport (HCPoly/Entry/Statements/TwoGridTransport.lean) after ∃ C, 1 ≤ C ∧ ∃ Csrc, 0 < Csrc ∧, verbatim.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.HighContrast.Multiscale.BridgeBody (d : ℕ) (γ : ℝ) (L₀ : ℕ) (c₀ Csrc : ℝ) (B₀ : ℝ → ℕ → ℝ) : Prop

The body of Entry.successful_short_bridge (HCPoly/Entry/Statements/SuccessfulShortBridge.lean) after ∃ L₀ c₀, c₀ ∈ Ioo 0 1 ∧ ∃ Csrc, 0 < Csrc ∧, with the inner ∃ B₀ Skolemized into the function B₀ : ℝ → ℕ → ℝ of (σ, L); otherwise verbatim.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.Multiscale.selectionLength (L₀ : ℕ) (σ : ℝ) : ℕ

The selection length L = L₀ + ⌈(3/2) log₃(σ⁻¹)⌉ of e.bridge.length.choice (p.scale.selection). It does not depend on ε.

Equations

• HCPolySupport.HighContrast.Multiscale.selectionLength L₀ σ = L₀ + ⌈3 / 2 * Real.logb 3 σ⁻¹⌉₊