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

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

The two input statements and the law-side support

Groups B and C of the printed proof: nonnegativity of the synchronized log-determinant loss, defined near e.scale.selection.logdet.loss, and — as a consequence proved by the cited bridge support lemmas below — of 𝒫 + D (profile plus determinant drift, defined near e.scale.selection.fluctuation.history), the Skolemized short-bridge statement (p.successful.short.bridge), the three source-constant monotonicity lemmas, and the two input statements repeated at their exact types and applied.

Part of the proof of p.scale.selection (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.

Group B — support with the law

theorem HCPolySupport.HighContrast.Multiscale.synchronizedLogDetLoss_nonneg (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hjStar : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (h n : ℤ) (h0 : 0 ≤ h) (hn : ↑jStar + h ≤ n + 1) : 0 ≤ synchCharge P (Geometry.explicitRoundedGrid jStar m) h n

Δ̂^q_h(n) ≥ 0 when every increment starts at or above j_* (near e.scale.selection.logdet.loss, via Annealed.logDetLoss_nonneg).

theorem HCPolySupport.HighContrast.Multiscale.profile_add_determinantDrift_nonneg (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (k n : ℤ) (hk : ↑jStar ≤ k) (hkn : k ≤ n) : 0 ≤ profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k n + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n

theorem HCPolySupport.HighContrast.Multiscale.bridge_skolem (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (L₀ : ℕ), ∃ c₀ ∈ Set.Ioo 0 1, ∃ (Csrc : ℝ), 0 < Csrc ∧ ∃ (B₀ : ℝ → ℕ → ℝ), BridgeBody d γ L₀ c₀ Csrc B₀

p.successful.short.bridge: the short-bridge statement with its B₀(σ,L) Skolemized.

theorem HCPolySupport.HighContrast.Multiscale.oneGridBody_mono_src (d : ℕ) (γ Csrc Csrc' C : ℝ) (hle : Csrc ≤ Csrc') (hbody : OneGridBody d γ Csrc C) : OneGridBody d γ Csrc' C

Monotonicity in Csrc: a body at a smaller Csrc is a body at a larger one (1 < K gives log₃(2K) ≥ 0).

theorem HCPolySupport.HighContrast.Multiscale.transportBody_mono_src (d : ℕ) (γ C Csrc Csrc' : ℝ) (hle : Csrc ≤ Csrc') (hbody : TransportBody d γ C Csrc) : TransportBody d γ C Csrc'

theorem HCPolySupport.HighContrast.Multiscale.bridgeBody_mono_src (d : ℕ) (γ : ℝ) (L₀ : ℕ) (c₀ Csrc Csrc' : ℝ) (B₀ : ℝ → ℕ → ℝ) (hle : Csrc ≤ Csrc') (hbody : BridgeBody d γ L₀ c₀ Csrc B₀) : BridgeBody d γ L₀ c₀ Csrc' B₀

Group C — the two input statements, repeated at their exact types

theorem HCPolySupport.HighContrast.Multiscale.one_grid_provider_input (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∃ (C : ℝ), 0 < C ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K S → ∀ (h : ℕ), 2 * bigQ d γ ≤ h → ∀ (L : ℤ), 1 ≤ L → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (metric : Mat d), Matrix.PosDef metric → ∀ (n m : ℤ), ↑jStar ≤ n → n ≤ m → history P γ (Geometry.explicitRoundedGrid jStar metric) jStar m ≤ C * profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n m ∧ (n + ↑h ≤ m → profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n (m + ↑h) ≤ 1 / 8 * Real.exp (↑(bigQ d γ) * synchCharge P (Geometry.explicitRoundedGrid jStar metric) (↑h) m) * profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n m + C * (Real.exp (↑(bigQ d γ) * synchCharge P (Geometry.explicitRoundedGrid jStar metric) (↑h) m) - 1)) ∧ (n + ↑h ≤ m → profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n m ≤ 1 → profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n (m + L) ≤ C * ↑L * (profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n m + Real.exp (↑(bigQ d γ) * detIncrement P (Geometry.explicitRoundedGrid jStar metric) m (m + L)) - 1)) ∧ (m = n → history P γ (Geometry.explicitRoundedGrid jStar metric) jStar n ≤ 1 → profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n (n + L) ≤ C * ↑L * (history P γ (Geometry.explicitRoundedGrid jStar metric) jStar n + Real.exp (↑(bigQ d γ) * detIncrement P (Geometry.explicitRoundedGrid jStar metric) n (n + L)) - 1)) ∧ fluctuationHistory P γ (Geometry.explicitRoundedGrid jStar metric) jStar m + meanHistory P γ (Geometry.explicitRoundedGrid jStar metric) (↑jStar) m + determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar m ≤ C * (profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n m + determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar m) ∧ (n + ↑h ≤ m → profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n (m + ↑h) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar (m + ↑h) ≤ 1 / 8 * Real.exp (↑(bigQ d γ) * synchCharge P (Geometry.explicitRoundedGrid jStar metric) (↑h) m) * (profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n m + determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar m) + C * (Real.exp (↑(bigQ d γ) * synchCharge P (Geometry.explicitRoundedGrid jStar metric) (↑h) m) - 1)) ∧ (∀ (m₀ : ℤ), ↑jStar + ↑h ≤ m₀ → ∀ (Ksteps : ℕ), 1 ≤ Ksteps → ∑ k ∈ Finset.range Ksteps, synchCharge P (Geometry.explicitRoundedGrid jStar metric) (↑h) (m₀ + ↑k * ↑h) ≤ ↑h * detIncrement P (Geometry.explicitRoundedGrid jStar metric) (m₀ + 1 - ↑h) (m₀ + ↑Ksteps * ↑h)) ∧ (m = n ∨ n + ↑h ≤ m → profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n m + determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar m ≤ 1 → profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n (m + L) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar (m + L) ≤ C * ↑L * (profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n m + determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar m + Real.exp (↑(bigQ d γ) * detIncrement P (Geometry.explicitRoundedGrid jStar metric) m (m + L)) - 1))

The exact type of p.fixed.geometry.one.grid.propagation (HCPoly/Entry/Statements/OneGridPropagation.lean), applied from Entry.fixed_geometry_one_grid_propagation_full (HCPoly/Entry/OneGridPropagation.lean).

theorem HCPolySupport.HighContrast.Multiscale.two_grid_transport_provider_input (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ ρ ∈ Set.Ioc 0 1, ∀ δ ∈ Set.Icc 0 (1 / 4), ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K S → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (m mPlus : Mat d), Matrix.PosDef m → Matrix.PosDef mPlus → ∀ (k n : ℤ), ↑jStar ≤ k → k ≤ n → ∀ (L : ℕ), adaptedCell (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑L) ∪ adaptedCell (Geometry.explicitRoundedGrid jStar mPlus) (n + ↑L) ⊆ centeredCube d (2 * ↑jStar) → C * (↑L + Real.logb 3 ((2 + aspectRatio E) * (‖m‖ * ‖m⁻¹‖))) ≤ ↑n - ↑jStar → projectiveDistance m mPlus ≤ 1 → C + Real.logb 3 ρ⁻¹ ≤ ↑L → profile P γ (Geometry.explicitRoundedGrid jStar m) jStar k (n + 2 * ↑L) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar (n + 2 * ↑L) ≤ 3 ^ (-(1 / 2) * (1 - γ) * ↑L) * ρ → BlockMatLoewnerLE (blockScale (1 - δ) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑L))) (adaptedMean P (Geometry.explicitRoundedGrid jStar mPlus) (n + ↑L)) → BlockMatLoewnerLE (adaptedMean P (Geometry.explicitRoundedGrid jStar mPlus) (n + ↑L)) (blockScale (1 + δ) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑L))) → profile P γ (Geometry.explicitRoundedGrid jStar mPlus) jStar (n + ↑L) (n + ↑L) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar mPlus) jStar (n + ↑L) ≤ C * (δ + ρ)

The exact type of p.two.grid.transport (HCPoly/Entry/Statements/TwoGridTransport.lean), applied from Entry.two_grid_transport (HCPoly/Entry/TwoGridTransport.lean).

theorem HCPolySupport.HighContrast.Multiscale.one_grid_body_input (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∃ (C : ℝ), 0 < C ∧ OneGridBody d γ Csrc C

The one-grid input as a OneGridBody, one term conversion of one_grid_provider_input.

theorem HCPolySupport.HighContrast.Multiscale.two_grid_transport_body_input (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (Csrc : ℝ), 0 < Csrc ∧ TransportBody d γ C Csrc

The transport input as a TransportBody, one term conversion of two_grid_transport_provider_input.