Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section24.Sensitivity.Provider.Lambda.Closure

Closure #

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

The conditional lambda_{s,q} sensitivity provider #

Source: ABK26 (l.lambda.sensitivity).

This module discharges the two inputs of Provider.Lambda.Spine.unitCubeLambda_inv_perturb_le_of_cube_dhFluxForm_bound and assembles the provider form of the frozen target Algsuperdiff.Frozen.Section24.lambda_sensitivity.

The descendant scaling #

Provider.Lambda.CubeBound gives, on every triadic descendant R of the unit cube at scale k ≤ 0,

|D_h(R)[(0,-w)]| ≤ C(d) ‖∇h‖ · 3^k · λ_{3/8,2}^{-1}(R) · J(R) .

3^k · 3^{-3k/4} = 3^{k/4} ≤ 1   for k ≤ 0 ,

so the whole descendant family obeys the root-gauge bound consumed by the spine.

Descendant scaling of the coarse gauge #

source
theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.le_finsetSupReal' {α : Type u_1} (s : Finset α) (f : α → ℝ) {R : α} (hR : R ∈ s) :
f R ≤ HCPolySupport.Book.Ch02.finsetSupReal s f
source
theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.cubeScaleFactor_mul_multiscaleDescendantWeight_le_one {d : ℕ} {k : ℤ} (hk : k ≤ (HCPolySupport.originCube d 0).scale) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) k) :
HCPolySupport.cubeScaleFactor R * HCPolySupport.Book.Ch02.multiscaleDescendantWeight (HCPolySupport.originCube d 0) k (3 / 8) ≤ 1

The descendant scaling identity. On a triadic descendant of the unit cube at a nonpositive scale, the cube diameter exactly compensates the descendant loss of the coarse gauge.

source
theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.cubeScaleFactor_mul_lambdaSq_inv_le {d : ℕ} [NeZero d] (G : HCPolySupport.Book.Ch03.CoeffFamily d) {k : ℤ} (hk : k ≤ (HCPolySupport.originCube d 0).scale) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) k) :
HCPolySupport.cubeScaleFactor R * (HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) G)⁻¹ ≤ (HCPolySupport.Book.Ch02.lambdaSq (HCPolySupport.originCube d 0) (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) G)⁻¹

Root-gauge control of the descendant gauge.

The spine constant #

source
noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxSpineConst (d : ℕ) :
ℝ

The constant of the pure-flux descendant D_h bound, normalized so that it is at least one.

Equations
Instances For
    source
    theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.one_le_fluxSpineConst (d : ℕ) :
    1 ≤ fluxSpineConst d
    source
    theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxSpineConst_pos (d : ℕ) :
    0 < fluxSpineConst d
    source
    theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxCubeConst_le_two_mul_fluxSpineConst (d : ℕ) :
    fluxCubeConst d ≤ 2 * fluxSpineConst d

    The descendant D_h bound with the root gauge #

    source
    theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.abs_dhFluxForm_le_root_gauge {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (F : HCPolySupport.Book.Ch03.CoeffFamily d) (hF : (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.toLInfSkewMatrixFieldOn) τ) (descendantField hk hR h.toLInfSkewMatrixFieldOn) w| ≤ 2 * (fluxSpineConst d * h.gradientW1Infinity * pathGauge a h.toLInfSkewMatrixFieldOn τ) * HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) (descendantField hk hR h.toLInfSkewMatrixFieldOn) τ) 0 w

    The hcube input of the spine. On every triadic descendant of the unit cube, along the whole perturbation path, the pure-flux D_h form is controlled by the root coarse gauge.

    The provider #

    source
    theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.lambda_sensitivity {d : ℕ} (dimension : 2 ≤ d) :
    ∃ (C : ℝ), 0 < C ∧ ∀ (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d), h.gradientW1Infinity ≤ C⁻¹ * Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a → ∀ (s : ℝ) (q : HCPolySupport.Book.Ch02.MultiscaleExponent), 0 < s → s ≤ 1 / 2 → q.IsAdmissible → (Frozen.Section24.unitCubeLambda s q (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a h.toLInfSkewMatrixFieldOn 1))⁻¹ ≤ (1 + C * h.gradientW1Infinity * (Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹) * (Frozen.Section24.unitCubeLambda s q a)⁻¹

    The conditional lambda_{s,q} sensitivity estimate.

    This is the provider form of the frozen target Algsuperdiff.Frozen.Section24.lambda_sensitivity, with exactly the frozen binders.