CubeFieldData

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

The frozen perturbation restricted to a sub-cube

The p = 0 descendant-cube D_h bound applies the splitting identity, the weak integration by parts and the Besov product estimate on a sub-cube R of the frozen unit-cube carrier. Every analytic datum needed there is the restriction of a datum of the frozen UnitCubeSkewW2Infinity structure:

• the weak first-derivative data unitCubeDerivData h is a single global function of x; its L^∞ memberships restrict by measure monotonicity and its weak-derivative property restricts by HasWeakPartialDerivOn.restrict;
• the entrywise Lipschitz representatives supplied by Provider.DhBound.Lipschitz.UnitCube are globally Lipschitz functions on Vec d, so the Lipschitz hypothesis of the Besov product estimate holds on every sub-cube verbatim;
• the frozen L^∞ bound gradientW1Infinity is an a.e. bound on the whole carrier, hence on every sub-cube.

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

Restriction of the frozen weak-derivative data

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.memLp_firstDeriv_restrict {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) {V : Set (HCPolySupport.Vec d)} (hsub : V ⊆ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) (k i j : Fin d) : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => DhBound.unitCubeDerivData h k x i j) ⊤ (HCPolySupport.volumeMeasureOn V)

The L^∞ memberships of the frozen first derivative restrict to any sub-carrier.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.hasWeakPartialDeriv_value_restrict {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (hsub : V ⊆ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) (k i j : Fin d) : HCPolySupport.HasWeakPartialDerivOn V k (fun (x : HCPolySupport.Vec d) => ↑↑h.toLInfSkewMatrixFieldOn x i j) fun (x : HCPolySupport.Vec d) => DhBound.unitCubeDerivData h k x i j

The frozen weak-derivative identity restricts to any open sub-carrier.

Globally Lipschitz representatives of the first derivative

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

The entrywise globally Lipschitz representative of the frozen first-derivative field.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxDerivRep h k i j = ⋯.choose

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxDerivRep_lipschitz {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (k i j : Fin d) (x y : HCPolySupport.Vec d) : |fluxDerivRep h k i j x - fluxDerivRep h k i j y| ≤ ↑d * h.gradientW1Infinity * ‖x - y‖

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxDerivRep_ae_eq {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (k i j : Fin d) : (fun (x : HCPolySupport.Vec d) => fluxDerivRep h k i j x) =ᵐ[HCPolySupport.volumeMeasureOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier] fun (x : HCPolySupport.Vec d) => DhBound.unitCubeDerivData h k x i j

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

The globally Lipschitz representative of the weak divergence ∇·h.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxDivRep h x j = ∑ i : Fin d, Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxDerivRep h i i j x

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.matWeakDiv_unitCubeDerivData_apply' {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (x : HCPolySupport.Vec d) (j : Fin d) : DhBound.matWeakDiv (DhBound.unitCubeDerivData h) x j = ∑ i : Fin d, DhBound.unitCubeDerivData h i x i j

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxDivRep_lipschitz {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (x y : HCPolySupport.Vec d) : ‖fluxDivRep h x - fluxDivRep h y‖ ≤ ↑d ^ 2 * h.gradientW1Infinity * ‖x - y‖

Transfer to a sub-cube

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxDivRep_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) : fluxDivRep h =ᵐ[HCPolySupport.normalizedCubeMeasure R] DhBound.matWeakDiv (DhBound.unitCubeDerivData h)

The Lipschitz representative of ∇·h agrees a.e. with the weak divergence on every sub-cube of the frozen carrier.

L^∞ bounds on a sub-cube

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.toReal_eLpNorm_matrixDerivativeNorm_le_grad {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) : (MeasureTheory.eLpNorm (fun (x : HCPolySupport.Vec d) => Frozen.Section24.matrixDerivativeNorm (h.firstDeriv x)) ⊤ (HCPolySupport.volumeMeasureOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier)).toReal ≤ h.gradientW1Infinity

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.ae_abs_unitCubeDerivData_le_grad {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (k i j : Fin d) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier, |DhBound.unitCubeDerivData h k x i j| ≤ h.gradientW1Infinity

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.ae_norm_matWeakDiv_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) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.normalizedCubeMeasure R, ‖DhBound.matWeakDiv (DhBound.unitCubeDerivData h) x‖ ≤ ↑d * h.gradientW1Infinity

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.cubeLpNorm_infty_matWeakDiv_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) : HCPolySupport.cubeLpNorm R ⊤ (DhBound.matWeakDiv (DhBound.unitCubeDerivData h)) ≤ ↑d * h.gradientW1Infinity

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.cubeLpNorm_infty_fluxDivRep_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) : HCPolySupport.cubeLpNorm R ⊤ (fluxDivRep h) ≤ ↑d * h.gradientW1Infinity

L^∞ memberships on a sub-cube

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.memLp_unitCubeDerivData_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) (k i j : Fin d) (r : ENNReal) : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => DhBound.unitCubeDerivData h k x i j) r (HCPolySupport.normalizedCubeMeasure R)

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.memLp_matWeakDiv_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) (r : ENNReal) : MeasureTheory.MemLp (DhBound.matWeakDiv (DhBound.unitCubeDerivData h)) r (HCPolySupport.normalizedCubeMeasure R)

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.memLp_fluxDivRep_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) : MeasureTheory.MemLp (fluxDivRep h) ⊤ (HCPolySupport.normalizedCubeMeasure R)