High-contrast homogenization: Entry.Response.Transfer.AdaptedResponseAssembly

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

Assembling the adapted response decomposition

This file proves adapted_response_core, the decomposition claimed in the response transfer skeleton, from its eleven constituent lemmas — the block algebra, the energy estimate, the diagonal weak estimate, and the cutoff estimate — with no further unproved step of its own; the substitution of p.response.transfer into that decomposition is carried out here in full. Closing this substitution needs the same scalar arithmetic that turns a one-step contraction inequality κ_t - 1 ≤ ω κ_t into the target bound κ_t ≤ 1 + δ_ad, together with the parameter choice of the scale H, the tolerance η, and the base scale σ₀ that keeps the resulting contraction constant small enough; both are supplied here as the completeness check of the whole assembly.

Assembly of adapted_response_core

adapted_response_core_of_holes is adapted_response_core of HCPoly/Entry/Multiscale/ResponseTransferSkeleton.lean, proved -- with no sorry of its own -- from the eleven lemmas of CenteredEnergyIdentity, LoadMeanIdentity, WeakEstimateAssembly, ResponseCutoffEstimate. It is the completeness check of the assembly: the substitution of p.response.transfer is carried out here in full.

response_tolerances is not used: it converts delta into delta_ad, while adapted_response_core receives delta_ad directly. The lemmas of EccentricityScaleDecay.lean are not used here either: they are ingredients of the source smallness estimate, whose output is all the assembly needs.

Arithmetic helpers

The assembly

theorem HCPolySupport.HighContrast.Multiscale.adapted_response_core_of_holes (d : ℕ) (_hd : 2 ≤ d) (γ : ℝ) (_hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (_hS : S.Selects d γ) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ ε ∈ Set.Ioc 0 S.eps0, ∀ δad ∈ 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 ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ) (B : ℝ) (jStar : ℕ) (F : BlockMat d) (s t : ℤ), RawOutput d γ S ε σ Cglob Cprof Csrc H Bresp P E Ψ K Src B jStar F s t → canonicalImbalance (adaptedMean P (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) t) ≤ 1 + δad

adapted_response_core (HCPoly/Entry/Multiscale/ResponseTransferSkeleton.lean), proved from the eleven lemmas. Conclusion e.response.adapted.conclusion (e.response.adapted.conclusion).