DescendantBridge

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

From per-descendant pure-flux ratios to the frozen unitCubeLambda ratio

Source: ABK26. Having applied the D_h bound at p = 0 on every triadic descendant R of the unit cube, the source aggregates the resulting one-cube ratios into a ratio for lambda_{s,q}^{-1}.

This module performs that aggregation once and for all, at an arbitrary pair of path parameters t₁ ≤ t₂ (the source's tau and tau + dtau). The chain is

J(R; a + t₂ h; 0, w) ≤ rho · J(R; a + t₁ h; 0, w)   (all descendants R, all w)
  ⟹ |sigma_*^{-1}(R; a + t₂ h)| ≤ rho · |sigma_*^{-1}(R; a + t₁ h)|
                                                    (Provider.Lambda.CubeRatio)
  ⟹ lambda_{s,q}^{-1}(a + t₂ h)   ≤ rho · lambda_{s,q}^{-1}(a + t₁ h)
                                        (Multiscale.DescendantRatio, all
                                         admissible q including infinity)

The middle step needs the descendant localization of the perturbation (Multiscale.UnitCubeTransfer.coeffOn_descendant_aeeq_perturbCoeffOn), which is already available at an arbitrary path parameter.

Every declaration is an internal helper for the Section 2.4 sensitivity providers. The per-cube hypothesis is the analytic input; it is discharged at every application.

@[reducible, inline]

noncomputable abbrev Algsuperdiff.Section24.Sensitivity.Provider.Lambda.descendantField {d : ℕ} {k : ℤ} (hk : k ≤ (HCPolySupport.originCube d 0).scale) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) k) (h : Frozen.Section24.LInfSkewMatrixFieldOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) : Frozen.Section24.LInfSkewMatrixFieldOn (HCPolySupport.Book.Ch02.cubeDomain R)

The restriction of a unit-cube skew field to a triadic descendant.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.Lambda.descendantField hk hR h = Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.restrictLInfSkewMatrixFieldOn ⋯ h

One descendant cube

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.coarseSigmaStarInvMatrixNorm_le_of_cube_responseJ_ratio {d : ℕ} (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.LInfSkewMatrixFieldOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (t₁ t₂ : ℝ) (F G₁ G₂ : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (hF : (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a) (hG₁ : (G₁.coeffOn (HCPolySupport.originCube d 0)).AEEq (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a h t₁)) (hG₂ : (G₂.coeffOn (HCPolySupport.originCube d 0)).AEEq (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a h t₂)) {ρ : ℝ} (hρ : 0 ≤ ρ) {k : ℤ} (hk : k ≤ (HCPolySupport.originCube d 0).scale) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) k) (hJ : ∀ (w : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) (descendantField hk hR h) t₂) 0 w ≤ ρ * HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) (descendantField hk hR h) t₁) 0 w) : HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm R G₂ ≤ ρ * HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm R G₁

A pure-flux response ratio on a descendant cube, stated for the restricted perturbation path, is a one-cube sigma_*^{-1} ratio at the family level.

Aggregation to the frozen unit-cube gauge

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.unitCubeLambda_inv_le_of_cube_responseJ_ratio {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.LInfSkewMatrixFieldOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (t₁ t₂ : ℝ) {ρ s : ℝ} {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (hρ : 0 ≤ ρ) (hs : 0 < s) (hq : q.IsAdmissible) (hJ : ∀ (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d), (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a → ∀ (k : ℤ) (hk : k ≤ (HCPolySupport.originCube d 0).scale) (R : HCPolySupport.TriadicCube d) (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) k) (w : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) (descendantField hk hR h) t₂) 0 w ≤ ρ * HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) (descendantField hk hR h) t₁) 0 w) : (Frozen.Section24.unitCubeLambda s q (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a h t₂))⁻¹ ≤ ρ * (Frozen.Section24.unitCubeLambda s q (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a h t₁))⁻¹

The aggregated ratio for the frozen unitCubeLambda.

A uniform per-descendant, all-loadings pure-flux response ratio between the two path parameters t₁ and t₂ transfers verbatim to the frozen scalar unitCubeLambda s q for every s > 0 and every admissible q, including the endpoint q = infinity.