CubeTermA

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

Term A of the D_h split on a sub-cube of the frozen carrier

Source: ABK26, the second inequality of e.sensitivity.basic.split1, stated at an arbitrary triadic sub-cube R of the frozen unit cube.

Provider.DhBound.Discharge.InputA discharges the same two premises at the root cube. The only genuinely cube-dependent step is the positive Besov seminorm of a Lipschitz vector field, which carries one factor cubeScaleFactor R (Discharge.cubeBesovPositiveVectorPartialSeminormTwo_le_of_lipschitzOn, already stated at a general cube). Since cubeScaleFactor R ≤ 1 on descendants of the unit cube, the same constant Discharge.termABesovConst d works verbatim:

‖hᵀ p‖_{B^{3/8}_{2,2}(R)} ≤ termABesovConst d · |p| · ‖h‖_{W^{1,∞}(□₀)} .

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

A globally Lipschitz representative of the value field

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.potValueRep {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (i j : Fin d) : HCPolySupport.Vec d → ℝ

The entrywise globally Lipschitz representative of the frozen matrix field.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.potValueRep h i j = ⋯.choose

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.potValueRep_lipschitz {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (i j : Fin d) (x y : HCPolySupport.Vec d) : |potValueRep h i j x - potValueRep h i j y| ≤ ↑d * h.w1Infinity * ‖x - y‖

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.potValueRep_ae_eq_carrier {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (i j : Fin d) : (fun (x : HCPolySupport.Vec d) => potValueRep h i j x) =ᵐ[HCPolySupport.volumeMeasureOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier] fun (x : HCPolySupport.Vec d) => ↑↑h.toLInfSkewMatrixFieldOn x i j

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.potValueRep_ae_eq_cube {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (R : HCPolySupport.TriadicCube d) (hsub : (HCPolySupport.Book.Ch02.cubeDomain R).carrier ⊆ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) (i j : Fin d) : (fun (x : HCPolySupport.Vec d) => potValueRep h i j x) =ᵐ[HCPolySupport.normalizedCubeMeasure R] fun (x : HCPolySupport.Vec d) => ↑↑h.toLInfSkewMatrixFieldOn x i j

The Term A field and its representative on a sub-cube

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.potTermARep {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (p : HCPolySupport.Vec d) : HCPolySupport.Vec d → HCPolySupport.Vec d

The Lipschitz representative of the Term A field.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.potTermARep h p x i = ∑ j : Fin d, Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.potValueRep h j i x * p j

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.potTermARep_ae_eq_cube {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (p : HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) (hsub : (HCPolySupport.Book.Ch02.cubeDomain R).carrier ⊆ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) : potTermARep h p =ᵐ[HCPolySupport.normalizedCubeMeasure R] DhBound.Discharge.termAField h p

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.potTermARep_lipschitz {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (p x y : HCPolySupport.Vec d) : ‖potTermARep h p x - potTermARep h p y‖ ≤ ↑d ^ 2 * h.w1Infinity * HCPolySupport.Book.Ch02.vecNorm p * ‖x - y‖

L^p memberships and a.e. bounds on a sub-cube

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.memLp_value_entry_cube {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (R : HCPolySupport.TriadicCube d) (hsub : (HCPolySupport.Book.Ch02.cubeDomain R).carrier ⊆ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) (i j : Fin d) (r : ENNReal) : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => ↑↑h.toLInfSkewMatrixFieldOn x i j) r (HCPolySupport.normalizedCubeMeasure R)

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.memLp_termAField_component_cube {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (R : HCPolySupport.TriadicCube d) (hsub : (HCPolySupport.Book.Ch02.cubeDomain R).carrier ⊆ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) (p : HCPolySupport.Vec d) (i : Fin d) (r : ENNReal) : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => DhBound.Discharge.termAField h p x i) r (HCPolySupport.normalizedCubeMeasure R)

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.memLp_termAField_cube {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (R : HCPolySupport.TriadicCube d) (hsub : (HCPolySupport.Book.Ch02.cubeDomain R).carrier ⊆ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) (p : HCPolySupport.Vec d) (r : ENNReal) : MeasureTheory.MemLp (DhBound.Discharge.termAField h p) r (HCPolySupport.normalizedCubeMeasure R)

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.memLp_potTermARep_top_cube {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (R : HCPolySupport.TriadicCube d) (hsub : (HCPolySupport.Book.Ch02.cubeDomain R).carrier ⊆ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) (p : HCPolySupport.Vec d) : MeasureTheory.MemLp (potTermARep h p) ⊤ (HCPolySupport.normalizedCubeMeasure R)

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.ae_abs_termAField_le_cube {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (R : HCPolySupport.TriadicCube d) (hsub : (HCPolySupport.Book.Ch02.cubeDomain R).carrier ⊆ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) (p : HCPolySupport.Vec d) (i : Fin d) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.normalizedCubeMeasure R, |DhBound.Discharge.termAField h p x i| ≤ ↑d * h.w1Infinity * HCPolySupport.Book.Ch02.vecNorm p

The Term A Besov budget on a sub-cube

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.cubeBesovPositiveVectorPartialSeminormTwo_termAField_cube_le {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (R : HCPolySupport.TriadicCube d) (hsub : (HCPolySupport.Book.Ch02.cubeDomain R).carrier ⊆ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) (hL : HCPolySupport.cubeScaleFactor R ≤ 1) (p : HCPolySupport.Vec d) (N : ℕ) : HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo R (3 / 8) N (DhBound.Discharge.termAField h p) ≤ DhBound.Besov.besovPerturbConst (3 / 8) * (↑d ^ 2 * h.w1Infinity * HCPolySupport.Book.Ch02.vecNorm p)

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.forceBesovRegularity_termAField_cube {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (R : HCPolySupport.TriadicCube d) (hsub : (HCPolySupport.Book.Ch02.cubeDomain R).carrier ⊆ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) (hL : HCPolySupport.cubeScaleFactor R ≤ 1) (p : HCPolySupport.Vec d) : HCPolySupport.Book.Ch03.ForceBesovRegularity R (3 / 8) fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (HCPolySupport.matTranspose (↑↑h.toLInfSkewMatrixFieldOn x)) p

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.scaleNormalizedPositiveBesovVectorNormTwo_termAField_cube_le {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (R : HCPolySupport.TriadicCube d) (hsub : (HCPolySupport.Book.Ch02.cubeDomain R).carrier ⊆ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) (hL : HCPolySupport.cubeScaleFactor R ≤ 1) (p : HCPolySupport.Vec d) : (HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorNormTwo R (3 / 8) fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (HCPolySupport.matTranspose (↑↑h.toLInfSkewMatrixFieldOn x)) p) ≤ DhBound.Discharge.termABesovConst d * HCPolySupport.Book.Ch02.vecNorm p * h.w1Infinity

The Term A positive Besov budget on a sub-cube of the frozen carrier.