Closure

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

The Lambda_{s,2} sensitivity providers

Source: ABK26 (e.big.Lambda.sensitivity).

Both provider results are assembled from

• the descendant b-matrix estimate BigLambda.coarseBMatrixNorm_perturb_le,
• the geometric resummation of Provider.Multiscale.GeometricResummation (the fixed-factor version) resp. its general-coefficient form BigLambda.LambdaSq_two_le_of_descendant_bound_coeff, and
• the root transfer Provider.Multiscale.unitCubeBigLambda_le_of_family_bound.

The frozen constant

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.bigLambdaConst (d : ℕ) : ℝ

A common constant for the upper multiscale ellipticity sensitivity estimates.

Equations

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.bigLambdaConst_pos (d : ℕ) : 0 < bigLambdaConst d

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.bigLambdaGateConst_le_bigLambdaConst (d : ℕ) : bigLambdaGateConst d ≤ bigLambdaConst d

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.two_mul_potCubeConstA_sq_le_bigLambdaConst (d : ℕ) : 2 * potCubeConstA d ^ 2 ≤ bigLambdaConst d

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.two_mul_potCubeConstB_le_bigLambdaConst (d : ℕ) : 2 * potCubeConstB d ≤ bigLambdaConst d

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.bigLambdaGate_of_frozen_gate {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (hgate : h.gradientW1Infinity ≤ (bigLambdaConst d)⁻¹ * Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a) : h.gradientW1Infinity ≤ (bigLambdaGateConst d)⁻¹ * Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a

The frozen gate implies the gate of BigLambda.CubeJSensitivity.

The fixed-factor provider

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.bigLambda_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 : ℝ), 0 < s → s < 3 / 8 → Frozen.Section24.unitCubeBigLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a h.toLInfSkewMatrixFieldOn 1) ≤ 4 * Frozen.Section24.unitCubeBigLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a + C * (3 / 8 - s)⁻¹ * h.w1Infinity ^ 2 * (Frozen.Section24.unitCubeLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹

Fixed-factor sensitivity of Lambda_{s,2}.

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

The free-δ provider

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.bigLambda_sensitivity_at_delta {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 δ : ℝ), 0 < s → s < 3 / 8 → 0 < δ → δ ≤ 1 → Frozen.Section24.unitCubeBigLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (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.unitCubeBigLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a + C * δ⁻¹ * (3 / 8 - s)⁻¹ * h.w1Infinity ^ 2 * (Frozen.Section24.unitCubeLambda s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹

Free-δ sensitivity of Lambda_{s,2}.

This is the provider form of the frozen target Algsuperdiff.Frozen.Section24.bigLambda_sensitivity_at_delta, with exactly the frozen binders and the range 0 < δ ≤ 1.