High-contrast homogenization: Entry.ResponseTransfer

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

p.response.transfer

HCPolySupport.HighContrast.Entry.response_transfer is the statement of HCPolySupport.HighContrast.response_transfer (HCPoly/Entry/Statements/ResponseTransfer.lean). Its statement is the one, character for character; the statement file's body is one by exact application of this theorem to that statement's binders.

The proof is the assembly of p.response.transfer over the four kernels and the bookkeeping lemmas of HCPoly/Entry/Multiscale/ResponseTransferSkeleton.lean, which this file imports.

theorem HCPolySupport.HighContrast.Entry.response_transfer (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (hS : S.Selects d γ) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ ε ∈ Set.Ioc 0 S.eps0, ∀ δ ∈ Set.Ioc 0 1, ∃ (H : ℕ), max 4 S.h ≤ H ∧ ∀ (Cprof : ℝ), 0 < Cprof → ∃ σ₀ ∈ Set.Ioc 0 ε, ∀ σ ∈ Set.Ioc 0 σ₀, ∀ (Cglob : ℝ), 0 < Cglob → ∃ (Bresp : ℝ), 1 ≤ Bresp ∧ ∃ (Cresp : ℝ), 0 < Cresp ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (B : ℝ), max (S.B0 ε σ) Bresp ≤ B → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Cglob * (B + 1) * Real.logb 3 (2 + aspectRatio E) + Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (F : BlockMat d) (s t : ℤ), IsSymmetricBlockMat F → Book.Ch02.BlockPosDef F → s < t → t = s + ↑H → ↑jStar + ⌈B * Real.logb 3 (2 + aspectRatio E)⌉ ≤ s → t ≤ ↑jStar + ⌈(B + Cglob) * Real.logb 3 (2 + aspectRatio E)⌉ → adaptedCell (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) t ⊆ centeredCube d (2 * ↑jStar) → BlockMatLoewnerLE (blockScale (1 - √ε * σ) F) (adaptedMean P (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) s) → BlockMatLoewnerLE (adaptedMean P (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) s) (blockScale (1 + √ε * σ) F) → (↑d)⁻¹ * detIncrement P (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) s t < σ → max (max (profile P γ (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) jStar s s) (profile P γ (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) jStar s t)) (profile P γ (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) jStar t t) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) jStar s + determinantDrift P γ (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) jStar t ≤ Cprof * σ ^ ((1 - γ) / 8) → (‖explicitCanonicalMetric F‖ * ‖(explicitCanonicalMetric F)⁻¹‖) ^ (1 / 2) ≤ (2 + aspectRatio E) ^ Cglob → ∃ (mEnt : ℤ), t < mEnt ∧ ⋯ ∧ annealedContrast P mEnt - 1 ≤ δ

Proposition p.response.transfer. In the the generalized raw-output form, one source constant Csrc(d,γ) works for every raw ε ∈ (0,ε₀]; for every δ ∈ (0,1] there are H ≥ max {4,h} and σ₀ ∈ (0,ε] such that, for every σ ∈ (0,σ₀] and raw global constant Cglob, there are response constants Bresp ≥ 1 and Cresp < ∞ with: every qualifying global-selection output at B ≥ max {B₀,Bresp} admits a deterministic Euclidean generation m_ent > t satisfying m_ent - t ≤ ⌈Cresp log₃(2+Π)⌉ and Θ_{m_ent}-1 ≤ δ.

Assembly (p.response.transfer): Csrc := max of the two kernel source constants; tolerances from response_tolerances; H, σ₀, Bresp₁ from adapted_response_kernel; Bresp₂, Cresp from persistence_transfer_kernel; Bresp := max; unpack the binders into RawOutput, weaken by RawOutput.mono; mEnt := t + ℓ; widen the sandwich by blockScale_loewner_mono and loewner_trans; canonical_comparison_kernel, then euclidean_contrast_bridge_kernel with annealedContrast_eq and the third tolerance; generation bound by nat_le_ceil_of_le.