DoubledPairingCross

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

The cross term of Step 2 by the depth-zero Besov identity

Source display in ABK26: the cross-term estimate of Step 2 of l.approximate.recurrence.formula,

P_z . fint_{z+cu_n} bfA_m tilde S_z
  <= C | bfAhom^{1/2} P_z | Lambda-tilde 3^n [ bfAhom^{1/2} bfF_z ]_{H^1(z+cu_n)} .

The route

The manuscript reaches this display by Cauchy--Schwarz in the bfA_m-form followed by e.bound.one.cube.by.lambdas. That term is the plain cube average:

cubeBesovNegativeVectorPartialSeminormTwo Q s 0 u = || fint_Q u || ,

recorded here as cubeBesovNegativeVectorPartialSeminormTwo_zero. Hence any envelope Bu of the finite-depth negative seminorms of bfA_0^{-1/2} bfA_m tilde S_z already controls its cube average, and the cross term follows from Cauchy--Schwarz alone. Strictly fewer inputs than the printed route: no one-cube ellipticity comparison is spent here.

The statement below is gauge-neutral: it is proved for an arbitrary block vector P and an arbitrary block field Y. A caller instantiates it at P:= bfAhom^{1/2} P_z and Y:= bfAhom^{-1/2} bfA_m tilde S_z after applying DoubledPairingGauge.blockVecDot_blockGaugeDown_blockGaugeUp, so that normP becomes the manuscript's |bfAhom^{1/2} P_z| in the component-sum rendering. That instantiation is not performed here.

Binders

Bu is a caller-supplied envelope of the finite-depth negative seminorms. No smallness, moment, measurability or integrability proposition occurs: everything below is pointwise linear algebra and one identity of the seminorm at depth zero.

Scope

No anchor, frozen theorem or external input is consumed, and there is no sorry.

The depth-zero identity

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cubeBesovNegativeVectorDepthAverage_zero {d : ℕ} (Q : HCPolySupport.TriadicCube d) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) : HCPolySupport.cubeBesovNegativeVectorDepthAverage Q u 0 = HCPolySupport.vecNormSq (HCPolySupport.cubeAverageVec Q u)

The depth-zero negative Besov block average is the squared norm of the cube average.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cubeBesovNegativeVectorPartialSeminormTwo_zero {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) : HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s 0 u = HCPolySupport.Book.Ch02.vecNorm (HCPolySupport.cubeAverageVec Q u)

The identity. The finite-depth negative q = 2 Besov seminorm at depth 0 is the norm of the cube average.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.vecNorm_cubeAverageVec_le_of_partialSeminormTwo_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) {Bu : ℝ} (h : ∀ (N : ℕ), HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N u ≤ Bu) : HCPolySupport.Book.Ch02.vecNorm (HCPolySupport.cubeAverageVec Q u) ≤ Bu

A negative-seminorm envelope controls the cube average.

The cross term

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.blockVecNormSum {d : ℕ} (P : HCPolySupport.BlockVec d) : ℝ

The doubled block norm in the component-sum rendering.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.blockVecNormSum P = HCPolySupport.Book.Ch02.vecNorm P.1 + HCPolySupport.Book.Ch02.vecNorm P.2

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.blockVecNormSum_nonneg {d : ℕ} (P : HCPolySupport.BlockVec d) : 0 ≤ blockVecNormSum P

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.abs_blockVecDot_cubeAverage_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (P : HCPolySupport.BlockVec d) (Y : HCPolySupport.Vec d → HCPolySupport.BlockVec d) {Bu : ℝ} (hneg1 : ∀ (N : ℕ), (HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => (Y x).1) ≤ Bu) (hneg2 : ∀ (N : ℕ), (HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => (Y x).2) ≤ Bu) : |HCPolySupport.vecDot P.1 (HCPolySupport.cubeAverageVec Q fun (x : HCPolySupport.Vec d) => (Y x).1) + HCPolySupport.vecDot P.2 (HCPolySupport.cubeAverageVec Q fun (x : HCPolySupport.Vec d) => (Y x).2)| ≤ blockVecNormSum P * Bu

The cross term by the depth-zero route.

| P . fint_Q Y |  <=  blockVecNormSum P * Bu

for any envelope Bu of the finite-depth negative q = 2 Besov seminorms of the two legs of Y. Per the only ingredients are the depth-zero identity and Cauchy--Schwarz.