BlockBesovPositive

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

The positive block Besov seminorm and the block duality pairing

Step 2 of l.approximate.recurrence.formula pairs two doubled fields:

  fint_{z+cu_n} bfF_z . bfA_m tilde S_z
    <= [ bfAhom^{1/2} bfF_z ]_{Hbar^1(z+cu_n)}
       [ bfAhom^{-1/2} bfA_m tilde S_z ]_{Hbar^{-1}(z+cu_n)} .

BlockBesovSeminorm.lean supplies the negative half blockNegativeBesovTwo, in the component-sum rendering. This module supplies the doubled fluctuation and the pairing itself. The positive side is never packed into a block quantity: it enters componentwise, through CoarseGraining's cubeBesovPositiveVectorPartialSeminormTwo on each of the two blocks.

• blockCubeFluctuation -- the doubled cube fluctuation Y - fint_Q Y.
• abs_cubeAverage_blockVecDot_blockCubeFluctuation_le -- the block duality pairing, the sum of two copies of CoarseGraining's componentwise sharp q = 2 bound abs_cubeAverage_vecDot_fluctuationVec_le_sum_sharp_note_terms_of_partialBounds_two_two.

No new analysis occurs here: blockVecDot X Y = vecDot X.1 Y.1 + vecDot X.2 Y.2 is definitionally a two-term sum, and blockNegativeBesovTwo is definitionally the sum of the two component seminorms, so the block pairing is exactly the sum of two upstream Vec d pairings. This module is the carrier lift.

Feeding the partial-bound hypotheses

CoarseGraining's duality theorem consumes bounds on the finite-depth seminorms (... ≤ Bu for every truncation N), not on their suprema. The two _le_blockNegativeBesovTwo lemmas below produce exactly those on the negative side, from the block seminorm, given the BddAbove producers of TruncationPoincareBridge.lean. On the positive side the pairing takes the componentwise finite-depth bounds directly, as its binders hpos1 and hpos2.

References

• ABK26, l.approximate.recurrence.formula Step 2.

Additivity of the cube average

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cubeAverage_add_of_integrableOn {d : ℕ} (Q : HCPolySupport.TriadicCube d) (f g : HCPolySupport.Vec d → ℝ) (hf : MeasureTheory.IntegrableOn f (HCPolySupport.cubeSet Q) MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn g (HCPolySupport.cubeSet Q) MeasureTheory.volume) : (HCPolySupport.cubeAverage Q fun (x : HCPolySupport.Vec d) => f x + g x) = HCPolySupport.cubeAverage Q f + HCPolySupport.cubeAverage Q g

Additivity of cubeAverage under cube-set integrability.

The two doubled carriers

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.blockCubeFluctuation {d : ℕ} (Q : HCPolySupport.TriadicCube d) (G : HCPolySupport.Vec d → HCPolySupport.BlockVec d) : HCPolySupport.Vec d → HCPolySupport.BlockVec d

The doubled cube fluctuation of a block field: the componentwise Vec d fluctuations, packed.

Equations

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

From the block seminorms to the partial bounds

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cubeBesovNegativeVectorPartialSeminormTwo_fst_le_blockNegativeBesovTwo {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (F : HCPolySupport.Vec d → HCPolySupport.BlockVec d) (hbd : BddAbove (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => (F x).1)) (N : ℕ) : (HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => (F x).1) ≤ blockNegativeBesovTwo Q s F

The first component's finite-depth negative seminorms are bounded by the block seminorm.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cubeBesovNegativeVectorPartialSeminormTwo_snd_le_blockNegativeBesovTwo {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (F : HCPolySupport.Vec d → HCPolySupport.BlockVec d) (hbd : BddAbove (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => (F x).2)) (N : ℕ) : (HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => (F x).2) ≤ blockNegativeBesovTwo Q s F

The second component's finite-depth negative seminorms are bounded by the block seminorm.

The block duality pairing

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.abs_cubeAverage_blockVecDot_blockCubeFluctuation_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (F G : HCPolySupport.Vec d → HCPolySupport.BlockVec d) {Bu Bg : ℝ} (hs : 0 < s) (hF1 : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => (F x).1) 2 (HCPolySupport.normalizedCubeMeasure Q)) (hF2 : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => (F x).2) 2 (HCPolySupport.normalizedCubeMeasure Q)) (hG1 : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => (G x).1) 2 (HCPolySupport.normalizedCubeMeasure Q)) (hG2 : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => (G x).2) 2 (HCPolySupport.normalizedCubeMeasure Q)) (hBg : 0 ≤ Bg) (hInt1 : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (F x).1 (HCPolySupport.cubeFluctuationVec Q (fun (y : HCPolySupport.Vec d) => (G y).1) x)) (HCPolySupport.cubeSet Q) MeasureTheory.volume) (hInt2 : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (F x).2 (HCPolySupport.cubeFluctuationVec Q (fun (y : HCPolySupport.Vec d) => (G y).2) x)) (HCPolySupport.cubeSet Q) MeasureTheory.volume) (hneg1 : ∀ (N : ℕ), (HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => (F x).1) ≤ Bu) (hneg2 : ∀ (N : ℕ), (HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => (F x).2) ≤ Bu) (hpos1 : ∀ (N : ℕ), (HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => (G x).1) ≤ Bg) (hpos2 : ∀ (N : ℕ), (HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => (G x).2) ≤ Bg) : |HCPolySupport.cubeAverage Q fun (x : HCPolySupport.Vec d) => HCPolySupport.blockVecDot (F x) (blockCubeFluctuation Q G x)| ≤ 2 * (↑d * (3 ^ (↑d + s) * (HCPolySupport.cubeBesovScaleWeight (-s) Q * Bu) * (HCPolySupport.cubeBesovScaleWeight s Q * Bg)))

The block negative/positive Besov duality pairing (carrier).

The sum of two copies of CoarseGraining's componentwise sharp q = 2 bound, one per doubled component.

: the caller supplies the exponent window hs, the four L^2 memberships, the sign of Bg, the two integrabilities of the pairing integrands on the cube, and the four families of finite-depth seminorm bounds. These are exactly the hypotheses of the upstream componentwise theorem, doubled.