DescendantRatio

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Per-cube ratio aggregation for the lower coarse-grained ellipticity

The conditional sensitivity estimate for lambda_{s,q} is obtained by applying a one-cube estimate to every triadic descendant z + cube_n of the unit cube and then aggregating. The aggregation step is purely structural: if the one-cube observable |sigma_*^{-1}| of the perturbed field is bounded by a fixed factor rho times that of the base field on every descendant, then the same factor passes to the multiscale aggregate lambda_{s,q}^{-1} for every `s

0and every admissibleq, including the endpoint q = infinity`.

This is the exact replacement for the source's differentiation of lambda_{s,q}^{-1} in the perturbation parameter: the aggregate is an infinite weighted aggregate of finite maxima and is never claimed to be classically differentiable. Only per-cube ratio estimates enter.

Every declaration is an internal helper for the Section 2.4 sensitivity providers. The hypothesis hdesc is the per-cube analytic input supplied by the neighbouring modules; it must be discharged at every application.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.maxDescendantSigmaStarInv_le_of_descendant_ratio {d : ℕ} (Q : HCPolySupport.TriadicCube d) (A₀ A₁ : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {ρ : ℝ} (hρ : 0 ≤ ρ) {k : ℤ} (hk : k ≤ Q.scale) (hdesc : ∀ R ∈ HCPolySupport.descendantsAtScale Q k, HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm R A₁ ≤ ρ * HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm R A₀) : HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q k A₁ ≤ ρ * HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q k A₀

A per-descendant ratio estimate passes to the finite descendant maxima.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.lambdaSqFinite_inv_le_of_descendant_ratio {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (A₀ A₁ : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {ρ s q : ℝ} (hρ : 0 ≤ ρ) (hs : 0 < s) (hq : 1 ≤ q) (hdesc : ∀ k ≤ Q.scale, ∀ R ∈ HCPolySupport.descendantsAtScale Q k, HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm R A₁ ≤ ρ * HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm R A₀) : (HCPolySupport.Book.Ch02.lambdaSq Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite q) A₁)⁻¹ ≤ ρ * (HCPolySupport.Book.Ch02.lambdaSq Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite q) A₀)⁻¹

Finite-exponent ratio aggregation.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.lambdaSqInfinity_inv_le_of_descendant_ratio {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (A₀ A₁ : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {ρ s : ℝ} (hρ : 0 ≤ ρ) (hs : 0 < s) (hdesc : ∀ k ≤ Q.scale, ∀ R ∈ HCPolySupport.descendantsAtScale Q k, HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm R A₁ ≤ ρ * HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm R A₀) : (HCPolySupport.Book.Ch02.lambdaSq Q s HCPolySupport.Book.Ch02.MultiscaleExponent.infinity A₁)⁻¹ ≤ ρ * (HCPolySupport.Book.Ch02.lambdaSq Q s HCPolySupport.Book.Ch02.MultiscaleExponent.infinity A₀)⁻¹

Endpoint (q = infinity) ratio aggregation.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.lambdaSq_inv_le_of_descendant_ratio {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (A₀ A₁ : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {ρ s : ℝ} {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (hρ : 0 ≤ ρ) (hs : 0 < s) (hq : q.IsAdmissible) (hdesc : ∀ k ≤ Q.scale, ∀ R ∈ HCPolySupport.descendantsAtScale Q k, HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm R A₁ ≤ ρ * HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm R A₀) : (HCPolySupport.Book.Ch02.lambdaSq Q s q A₁)⁻¹ ≤ ρ * (HCPolySupport.Book.Ch02.lambdaSq Q s q A₀)⁻¹

Per-cube ratio aggregation. A uniform per-descendant ratio bound on the one-cube observable |sigma_*^{-1}| transfers verbatim to the multiscale aggregate lambda_{s,q}^{-1}, for every s > 0 and every admissible q (finite or the endpoint infinity). This is the aggregation step of the conditional lambda_{s,q} sensitivity estimate.