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

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

The selected output and the run

The profile bound satisfied by the selected output, the two inputs (p.scale.selection and p.initial.fixed.grid.scale), the predicate SelectedOutput describing the tuple the run produces, and the run itself.

§F Selected-output estimates (p.global.selection)

theorem HCPolySupport.HighContrast.Multiscale.output_profile_bound (Cout Cfs Cmaj Cexp Q ρ σ H d pss dss pts dt ptt Δ : ℝ) (hρ : 0 ≤ ρ) (hCout : 0 ≤ Cout) (hCfs : 0 ≤ Cfs) (hCmaj : 0 ≤ Cmaj) (hCexp : 0 ≤ Cexp) (hH : 0 ≤ H) (hQ : 0 ≤ Q) (hd : 0 ≤ d) (hσ : 0 ≤ σ) (hpss : 0 ≤ pss) (hdss : 0 ≤ dss) (hpts : 0 ≤ pts) (hdt : 0 ≤ dt) (hptt : 0 ≤ ptt) (hΔ0 : 0 ≤ Δ) (hΔ : Δ < d * σ) (h1 : pss + dss ≤ Cout * ρ) (h2 : pts + dt ≤ Cfs * H * (pss + dss + (Real.exp (Q * Δ) - 1))) (hexp : Real.exp (Q * d * σ) - 1 ≤ Cexp * ρ) (h3 : ptt ≤ Cmaj * pts) : max (max pss pts) ptt + dss + dt ≤ (2 * Cout + (2 + Cmaj) * Cfs * H * (Cout + Cexp)) * ρ

p.global.selection (e.global.selection.profile), scalar assembly with ρ = σ^((1-γ)/8): change-of-geometry output pss + dss ≤ Cout ρ, fixed-span s → t with Δ_{s,t} < dσ, the exponential bound exp(Qdσ) - 1 ≤ Cexp ρ, majorization ptt ≤ Cmaj pts. The resulting Cprof = 2 Cout + (2 + Cmaj) Cfs H (Cout + Cexp) is free of σ.

§G The proposition inputs and the run assembly

theorem HCPolySupport.HighContrast.Multiscale.initial_provider_input (d : ℕ) (hd : 2 ≤ d) : ∃ (Cgeom : ℝ), 0 < Cgeom ∧ ∀ γ ∈ Set.Ico 0 1, ∀ (S : SelectionData), S.Selects d γ → ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ ηinit ∈ Set.Ioc 0 1, ∃ (C : ℝ), 0 < C ∧ ∀ (ε σ : ℝ), 0 < σ → σ ≤ ε → ε ≤ S.eps0 → ∀ (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 → ∀ (B : ℝ), S.B0 ε σ ≤ B → ∃ (n₀ : ℤ), ↑jStar + ⌈B * Real.logb 3 (2 + aspectRatio E)⌉ ≤ n₀ ∧ n₀ ≤ ↑jStar + ⌈B * Real.logb 3 (2 + aspectRatio E)⌉ + ⌈C * Real.logb 3 (2 + aspectRatio E)⌉ ∧ profile P γ 1 jStar n₀ n₀ + determinantDrift P γ 1 jStar n₀ ≤ ηinit ∧ BlockMatLoewnerLE (blockScale (1 / 2) (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat E)⁻¹ * toFullBlockMat (blockSwap d)))) (adaptedMean P 1 n₀) ∧ BlockMatLoewnerLE (adaptedMean P 1 n₀) (blockScale 2 E) ∧ projectiveDistance 1 (explicitCanonicalMetric (adaptedMean P 1 n₀)) ≤ Cgeom * Real.log (2 + 4 * aspectRatio E)

p.initial.fixed.grid.scale, exact type declared in HCPoly/Entry/Statements/InitialFixedGridScale.lean; applies Entry.initial_fixed_grid_scale directly.

def HCPolySupport.HighContrast.Multiscale.SelectedOutput {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ ε σ Cprof C : ℝ) (E : BlockMat d) (H jStar : ℕ) (B : ℝ) : Prop

The output tuple of the run (p.global.selection), as a predicate, so global_run and global_selection share one interface.

Equations

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