Product

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

The Besov product estimate e.besov.mult at the consuming exponents

Source: ABK26 (e.besov.mult) as consumed at e.split.besov.stuff inside the proof of l.Dh.bound.

The consuming instance is

‖ v ξ ‖_{B^{s}_{2,2}(□)}
  ≤ C ‖v‖_{L²(□)} ‖∇ξ‖_{L^∞(□)}  +  C ‖ξ‖_{L^∞(□)} [v]_{B^{s}_{2,2}(□)} ,

with a scalar multiplicand v ∈ L² and a vector multiplier ξ ∈ W^{1,∞}, at s = 3/8. This file proves exactly that split.

What is new here

CoarseGraining already proves the per-cube Hölder step with no regularity hypothesis (cubeLpNorm_two_cubeFluctuationVec_scalar_smul_le_note_terms), and it proves the multiscale assembly for a C^∞ multiplier (the smooth-multiplier cutoff estimate for the positive Besov partial seminorm). The sensitivity multiplier ∇ · h is only W^{1,∞}, so the smoothness hypothesis is unusable downstream. This file redoes the assembly with the multiplier regularity spelled as the convex-domain form of W^{1,∞}: a Lipschitz bound on the cube. On a convex set these are the same regularity class, and no proof step is smuggled into a hypothesis.

Structure

• cubeLpNorm_infty_sub_cubeAverageVec_le_cubeScaleFactor_mul_of_lipschitzOn — the oscillation of the multiplier on a cube;
• cubeLpNorm_two_cubeFluctuationVec_scalar_smul_le_of_lipschitzOn — one cube;
• cubeBesovPositiveVectorDepthSeminorm_scalar_smul_le_of_lipschitzOn — depth j;
• cubeBesovPositiveVectorPartialSeminormTwo_scalar_smul_le_of_lipschitzOn — finite-depth ℓ² assembly;
• cubeBesovPositiveVectorPartialSeminormTwo_scalar_smul_le_besovMult — the final e.besov.mult shape, with the L²-of-v factor.

Everything is stated at finite depth N, uniformly in N: the sSup (infinite-depth) version cannot be stated without carrying a BddAbove hypothesis, which the statement discipline forbids. This matches how CoarseGraining's own downstream consumers use the cutoff-product estimate.

Step 1: oscillation of a Lipschitz multiplier on a cube

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Besov.cubeLpNorm_infty_sub_cubeAverageVec_le_cubeScaleFactor_mul_of_lipschitzOn {d : ℕ} (Q : HCPolySupport.TriadicCube d) {ξ : HCPolySupport.Vec d → HCPolySupport.Vec d} {B : ℝ} (hB : 0 ≤ B) (hξLp : MeasureTheory.MemLp ξ ⊤ (HCPolySupport.normalizedCubeMeasure Q)) (hLip : ∀ x ∈ HCPolySupport.cubeSet Q, ∀ y ∈ HCPolySupport.cubeSet Q, ‖ξ x - ξ y‖ ≤ B * ‖x - y‖) : (HCPolySupport.cubeLpNorm Q ⊤ fun (x : HCPolySupport.Vec d) => ξ x - HCPolySupport.cubeAverageVec Q ξ) ≤ HCPolySupport.cubeScaleFactor Q * B

The L^∞ oscillation about the mean of a multiplier that is B-Lipschitz on the cube is at most the cube diameter times B. This is the only place the multiplier regularity is used; it replaces CoarseGraining's ContDiff route.

Step 2: the one-cube product estimate

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Besov.cubeLpNorm_two_cubeFluctuationVec_scalar_smul_le_of_lipschitzOn {d : ℕ} (Q : HCPolySupport.TriadicCube d) (v : HCPolySupport.Vec d → ℝ) (ξ : HCPolySupport.Vec d → HCPolySupport.Vec d) {B : ℝ} (hB : 0 ≤ B) (hv : MeasureTheory.MemLp v 2 (HCPolySupport.normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (HCPolySupport.normalizedCubeMeasure Q)) (hLip : ∀ x ∈ HCPolySupport.cubeSet Q, ∀ y ∈ HCPolySupport.cubeSet Q, ‖ξ x - ξ y‖ ≤ B * ‖x - y‖) : HCPolySupport.cubeLpNorm Q 2 (HCPolySupport.cubeFluctuationVec Q fun (x : HCPolySupport.Vec d) => v x • ξ x) ≤ 2 * (HCPolySupport.cubeScaleFactor Q * B * HCPolySupport.cubeLpNorm Q 2 v + HCPolySupport.cubeLpNorm Q ⊤ ξ * HCPolySupport.cubeBesovOscillation Q 2 v)

One-cube form of e.besov.mult for a B-Lipschitz vector multiplier.

Step 3: the depth-j estimate

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Besov.cubeBesovPositiveVectorDepthSeminorm_scalar_smul_le_of_lipschitzOn {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (j : ℕ) (v : HCPolySupport.Vec d → ℝ) (ξ : HCPolySupport.Vec d → HCPolySupport.Vec d) {B : ℝ} (hB : 0 ≤ B) (hv : MeasureTheory.MemLp v 2 (HCPolySupport.normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (HCPolySupport.normalizedCubeMeasure Q)) (hLip : ∀ x ∈ HCPolySupport.cubeSet Q, ∀ y ∈ HCPolySupport.cubeSet Q, ‖ξ x - ξ y‖ ≤ B * ‖x - y‖) : HCPolySupport.cubeBesovPositiveVectorDepthSeminorm Q s (fun (x : HCPolySupport.Vec d) => v x • ξ x) j ≤ 2 * (HCPolySupport.cubeScaleFactor Q * B * HCPolySupport.cubeL2ScalarDepthSeminorm Q (s - 1) v j + HCPolySupport.cubeLpNorm Q ⊤ ξ * HCPolySupport.cubeBesovPositiveScalarDepthSeminorm Q s v j)

Depth-j form of e.besov.mult for a B-Lipschitz vector multiplier.

Step 4: the finite-depth ℓ² assembly

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Besov.cubeBesovPositiveVectorPartialSeminormTwo_scalar_smul_le_of_lipschitzOn {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (N : ℕ) (v : HCPolySupport.Vec d → ℝ) (ξ : HCPolySupport.Vec d → HCPolySupport.Vec d) {B : ℝ} (hB : 0 ≤ B) (hv : MeasureTheory.MemLp v 2 (HCPolySupport.normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (HCPolySupport.normalizedCubeMeasure Q)) (hLip : ∀ x ∈ HCPolySupport.cubeSet Q, ∀ y ∈ HCPolySupport.cubeSet Q, ‖ξ x - ξ y‖ ≤ B * ‖x - y‖) : (HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => v x • ξ x) ≤ 2 * (HCPolySupport.cubeScaleFactor Q * B * HCPolySupport.cubeL2ScalarPartialSeminormTwo Q (s - 1) N v + HCPolySupport.cubeLpNorm Q ⊤ ξ * HCPolySupport.cubeBesovPositiveScalarPartialSeminormTwo Q s N v)

Finite-depth form of e.besov.mult for a B-Lipschitz vector multiplier.

Step 5: the e.besov.mult shape

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Besov.besovMultConst (s : ℝ) : ℝ

The constant produced by summing the geometric series ∑ 3^{2(s-1)j}.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Besov.besovMultConst s = 2 * √(1 - Real.rpow 3 (2 * (s - 1)))⁻¹

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Besov.besovMultConst_pos {s : ℝ} (hs : s < 1) : 0 < besovMultConst s

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Besov.cubeBesovPositiveVectorPartialSeminormTwo_scalar_smul_le_besovMult {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (N : ℕ) (v : HCPolySupport.Vec d → ℝ) (ξ : HCPolySupport.Vec d → HCPolySupport.Vec d) {B : ℝ} (hB : 0 ≤ B) (hs : s < 1) (hv : MeasureTheory.MemLp v 2 (HCPolySupport.normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (HCPolySupport.normalizedCubeMeasure Q)) (hLip : ∀ x ∈ HCPolySupport.cubeSet Q, ∀ y ∈ HCPolySupport.cubeSet Q, ‖ξ x - ξ y‖ ≤ B * ‖x - y‖) : (HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => v x • ξ x) ≤ besovMultConst s * (HCPolySupport.cubeScaleFactor Q * B * HCPolySupport.cubeLpNorm Q 2 v + HCPolySupport.cubeLpNorm Q ⊤ ξ * HCPolySupport.cubeBesovPositiveScalarPartialSeminormTwo Q s N v)

The Besov product estimate e.besov.mult at the consuming exponents p = q = 2, for a scalar multiplicand in L² and a B-Lipschitz (i.e. W^{1,∞}) vector multiplier, at finite depth.

This is the exact split used at e.split.besov.stuff: an L² norm of the multiplicand times the gradient bound of the multiplier, plus the L^∞ norm of the multiplier times the Besov seminorm of the multiplicand.