InputBC

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

Term BC: the positive Besov budget of x ↦ (w + w* + ℓ_p)(x) (∇·h)(x)

Source: ABK26 (e.split.besov.stuff.begin through e.split.besov.stuff). The second factor of the D_h split is the product of the zero-trace witness u with the weak divergence ∇·h. The source estimate is the Besov product rule e.besov.mult

‖u (∇·h)‖_{B^{3/8}_{2,2}} ≤ C ‖∇(∇·h)‖_{L^∞} ‖u‖_{L²} + C ‖∇·h‖_{L^∞} [u]_{B^{3/8}_{2,2}} ,

followed by the two u-estimates

‖u‖_{L²}            ≤ C [∇u]_{B^{-3/8}_{2,2}}      (`e.fractional.Sobolev.embedding.zero.bndr`, `t =
3/16`),
[u]_{B^{3/8}_{2,2}} ≤ C [∇u]_{B^{-3/8}_{2,2}}      (`l.Besov.grad.to.function` in the `ℓ²` form),

and the witness-gradient budget of Discharge.GradientSplit. Both W^{1,∞} norms of ∇·h are dominated by d (resp. d²) times the frozen gradientW1Infinity, so the whole Term BC budget is proportional to h.gradientW1Infinity · λ_{3/8,2}^{-1/2} (J^{1/2} + |p·q|^{1/2}), which is exactly the shape consumed by Assembly.abs_le_frozen_shape_of_budget_bounds.

The L^∞ half of the frozen gradient norm

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.toReal_eLpNorm_matrixDerivativeNorm_le_gradientW1Infinity {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.DhBound.Discharge.ae_abs_firstDeriv_le_gradientW1Infinity {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, |(h.firstDeriv x) (HCPolySupport.basisVec k) i j| ≤ h.gradientW1Infinity

The weak divergence field and its Lipschitz representative

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.derivRep {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (k i j : Fin d) (x : HCPolySupport.Vec d) : ℝ

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

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.derivRep h k i j x = ⋯.choose x

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.derivRep_ae_eq {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (k i j : Fin d) : (fun (x : HCPolySupport.Vec d) => derivRep h k i j x) =ᵐ[HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d 0)] fun (x : HCPolySupport.Vec d) => (h.firstDeriv x) (HCPolySupport.basisVec k) i j

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

The Lipschitz representative of the weak divergence ∇·h.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.divRep h x j = ∑ i : Fin d, Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.derivRep h i i j x

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.divRep_ae_eq {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) : divRep h =ᵐ[HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d 0)] matWeakDiv (unitCubeDerivData h)

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

L^∞ bounds for the weak divergence

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.memLp_firstDeriv_entry {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (k i j : Fin d) (r : ENNReal) : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => (h.firstDeriv x) (HCPolySupport.basisVec k) i j) r (HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d 0))

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.memLp_matWeakDiv_component {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (j : Fin d) (r : ENNReal) : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => matWeakDiv (unitCubeDerivData h) x j) r (HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d 0))

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.memLp_matWeakDiv {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (r : ENNReal) : MeasureTheory.MemLp (matWeakDiv (unitCubeDerivData h)) r (HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d 0))

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.memLp_divRep_top {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) : MeasureTheory.MemLp (divRep h) ⊤ (HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d 0))

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.ae_norm_matWeakDiv_le {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d 0), ‖matWeakDiv (unitCubeDerivData h) x‖ ≤ ↑d * h.gradientW1Infinity

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeLpNorm_infty_matWeakDiv_le {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) : HCPolySupport.cubeLpNorm (HCPolySupport.originCube d 0) ⊤ (matWeakDiv (unitCubeDerivData h)) ≤ ↑d * h.gradientW1Infinity

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeLpNorm_infty_divRep_le {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) : HCPolySupport.cubeLpNorm (HCPolySupport.originCube d 0) ⊤ (divRep h) ≤ ↑d * h.gradientW1Infinity

Elementary vector bookkeeping

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.sqrt_vecNormSq_le_sqrt_card_mul_norm {d : ℕ} (w : HCPolySupport.Vec d) : √(HCPolySupport.vecNormSq w) ≤ √↑d * ‖w‖

The two u-estimates

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.zeroTraceValueConst (d : ℕ) : ℝ

The constant of the zero-trace L² estimate at the gauge exponent.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.zeroTraceValueConst d = Algsuperdiff.Section24.Sensitivity.Provider.PairingConstants.zeroTraceValueConst d

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.zeroTraceValueConst_nonneg (d : ℕ) : 0 ≤ zeroTraceValueConst d

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeLpNorm_two_h10_originCube_le {d : ℕ} [NeZero d] (u : HCPolySupport.H10Function (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) : (HCPolySupport.cubeLpNorm (HCPolySupport.originCube d 0) 2 fun (x : HCPolySupport.Vec d) => u.toFun x) ≤ zeroTraceValueConst d * HCPolySupport.cubeBesovNegativeVectorSeminormTwo (HCPolySupport.originCube d 0) (3 / 8) fun (x : HCPolySupport.Vec d) => u.grad x

The zero-trace L² estimate at the gauge exponent 2t = 3/8.

The Term BC field

def Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.termBCField {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (u : HCPolySupport.H10Function (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) : HCPolySupport.Vec d → HCPolySupport.Vec d

The Term BC field x ↦ u(x) (∇·h)(x).

Equations

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.memLp_u_two {d : ℕ} (u : HCPolySupport.H10Function (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => u.toFun x) 2 (HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d 0))

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.memLp_termBCField_two {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (u : HCPolySupport.H10Function (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) : MeasureTheory.MemLp (termBCField h u) 2 (HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d 0))

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovPositiveVectorPartialSeminormTwo_termBCField_le {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (u : HCPolySupport.H10Function (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) (N : ℕ) : HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo (HCPolySupport.originCube d 0) (3 / 8) N (termBCField h u) ≤ Besov.besovMultConst (3 / 8) * ((↑d ^ 2 * h.gradientW1Infinity * HCPolySupport.cubeLpNorm (HCPolySupport.originCube d 0) 2 fun (x : HCPolySupport.Vec d) => u.toFun x) + ↑d * h.gradientW1Infinity * HCPolySupport.cubeBesovPositiveScalarPartialSeminormTwo (HCPolySupport.originCube d 0) (3 / 8) N fun (x : HCPolySupport.Vec d) => u.toFun x)

The finite-depth Besov product estimate for the Term BC field.

The Term BC budget

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.termBCBesovConst (d : ℕ) : ℝ

The explicit Term B constant.

Equations

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.depthDowngradeConst_nonneg (d : ℕ) : 0 ≤ depthDowngradeConst d

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.termBCBesovConst_nonneg (d : ℕ) : 0 ≤ termBCBesovConst d

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.scaleNormalizedPositiveBesovVectorNormTwo_termBCField_le {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (p q : HCPolySupport.Vec d) {vAdj : HCPolySupport.Book.Ch02.Solution (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a.transpose} {v : HCPolySupport.Book.Ch02.Solution (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a} (hvAdj : HCPolySupport.Book.Ch02.IsResponseMaximizer (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a.transpose p (-q) vAdj) (hv : HCPolySupport.Book.Ch02.IsResponseMaximizer (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a p q v) (u : HCPolySupport.H10Function (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) (hu : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier, u.grad x = 2⁻¹ • (vAdj.toH1.grad x + v.toH1.grad x) + p) : HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorNormTwo (HCPolySupport.originCube d 0) (3 / 8) (termBCField h u) ≤ termBCBesovConst d * h.gradientW1Infinity * (√(Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ * (√(HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a p q) + √|HCPolySupport.vecDot p q|))

The Term BC positive Besov budget.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.forceBesovRegularity_termBCField {d : ℕ} [NeZero d] (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (u : HCPolySupport.H10Function (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) : HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d 0) (3 / 8) (termBCField h u)

The Term B regularity package.