Engine

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

The ratio engine of the conditional lambda_{s,q} sensitivity estimate

Source: ABK26. This module assembles the two previous steps into the ratio engine consumed by Provider.Lambda.Bootstrap:

• on each triadic descendant R of the unit cube and at each loading w, the pure-flux response t ↦ J(R; a + t h; 0, w) is differentiable with derivative one half of the D_h flux form (Provider.Lambda.PathGronwall), so the per-cube D_h bound is a differential inequality, and Grönwall turns it into a multiplicative ratio over any subinterval;
• that ratio is uniform in R and w, so it aggregates to a ratio for lambda_{s,q}^{-1} (Provider.Lambda.DescendantBridge) at every s > 0 and every admissible q, including q = infinity.

The per-cube D_h bound is the analytic input hcube; it is a premise of the internal helpers here and is discharged where they are used. No aggregate is ever differentiated.

Every declaration is an internal helper for the Section 2.4 sensitivity providers.

The two path functions

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.Lambda.pathGauge {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 : ℝ) : ℝ

The frozen coarse gauge lambda_{3/8,2}^{-1} along the perturbation path.

Equations

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

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.Lambda.pathLambdaInv {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))) (s : ℝ) (q : HCPolySupport.Book.Ch02.MultiscaleExponent) (t : ℝ) : ℝ

The frozen coarse gauge lambda_{s,q}^{-1} along the perturbation path.

Equations

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.pathGauge_nonneg {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 : ℝ) : 0 ≤ pathGauge a h t

The per-cube Grönwall step

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.responseJ_cube_ratio_of_dhFluxForm_bound {d : ℕ} (dimension : 2 ≤ 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))) {K C t₁ t₂ : ℝ} (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {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) (ht : t₁ ≤ t₂) (hcube : ∀ (τ : ℝ), t₁ ≤ τ → τ ≤ t₂ → |dhFluxForm (HCPolySupport.Book.Ch02.cubeDomain R) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) (descendantField hk hR h) τ) (descendantField hk hR h) w| ≤ 2 * (K * C) * HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) (descendantField hk hR h) τ) 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 ≤ Real.exp (K * C * (t₂ - t₁)) * 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

The per-cube D_h bound at p = 0, valid along the whole path, is a Grönwall differential inequality for the pure-flux response and therefore gives a multiplicative ratio over any subinterval.

The aggregated ratio engine

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.pathLambdaInv_ratio_engine {d : ℕ} [NeZero d] (dimension : 2 ≤ 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))) {K s : ℝ} {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (hs : 0 < s) (hq : q.IsAdmissible) (hcube : ∀ (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), |dhFluxForm (HCPolySupport.Book.Ch02.cubeDomain R) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) (descendantField hk hR h) τ) (descendantField hk hR h) w| ≤ 2 * (K * pathGauge a h τ) * HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) (descendantField hk hR h) τ) 0 w) (t₁ t₂ C : ℝ) (_ht₁ : 0 ≤ t₁) (ht : t₁ ≤ t₂) (_ht₂ : t₂ ≤ 1) (hK : 0 ≤ K) (hC : ∀ (τ : ℝ), t₁ ≤ τ → τ ≤ t₂ → pathGauge a h τ ≤ C) : pathLambdaInv a h s q t₂ ≤ Real.exp (K * C * (t₂ - t₁)) * pathLambdaInv a h s q t₁

The ratio engine. Given the per-cube D_h bound at p = 0 on all triadic descendants and along the whole path, with the root gauge as the coefficient, the frozen aggregate lambda_{s,q}^{-1} satisfies a multiplicative ratio estimate on every subinterval of [0,1] on which the root gauge is bounded by C.