DoubledPairingGauge

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

The gauge conjugation of the Step-2 duality pairing

Source displays in ABK26:

• e.form.of.A.naught, the scalar reference matrix bfA_0 = diag(sigma_0, sigma_0^{-1}) with kappa_0 = 0;
• the first display of Step 2 of l.approximate.recurrence.formula,

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

What the module supplies

The manuscript passes silently from the ungauged pairing bfF_z. bfA_m tilde S_z to the gauged one, in which the negative seminorm is taken of bfAhom^{-1/2} bfA_m tilde S_z and the positive seminorm of bfAhom^{1/2} bfF_z. Because bfAhom_{m-h} is the scalar block matrix diag(sigma_0, sigma_0^{-1}) (e.homs.defs, and the two sentences), that passage is the exact pointwise identity

( bfA_0^{-1/2} u ) . ( bfA_0^{1/2} F ) = u . F ,

proved here as blockVecDot_blockGaugeDown_blockGaugeUp: the two diagonal factors sigma_0^{\pm 1/2} cancel leg by leg. No inequality is spent.

Composing it with the doubled duality bound of BlockBesovPositive.lean gives abs_cubeAverage_blockVecDot_le_besovDualityConst, which is with the manuscript's generic C pinned to besovDualityConst, and with the doubled seminorms rendered as component sums.

Mean-zeroness of bfF_z enters here, and only here: it is what makes the positive-seminorm leg a genuine cube fluctuation, so that the upstream duality theorem -- which pairs against cubeFluctuationVec -- applies to the pairing as printed.

Binders

0 < s is the Besov exponent window; 0 < sig0 is the positivity of the scalar sigma_0 of e.form.of.A.naught; the four L^2 memberships and the two integrabilities are the hypotheses of the upstream componentwise duality theorem; hzero1, hzero2 are the mean-zeroness of the background of e.Fz.def on its own cell. Bu and Bg are caller-supplied seminorm envelopes.

Scope

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

The scalar gauge bfA_0^{\pm 1/2}

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.blockGaugeUp {d : ℕ} (sig0 : ℝ) (X : HCPolySupport.BlockVec d) : HCPolySupport.BlockVec d

bfA_0^{1/2} at the scalar bfA_0 = diag(sigma_0, sigma_0^{-1}).

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.blockGaugeUp sig0 X = (√sig0 • X.1, (√sig0)⁻¹ • X.2)

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.blockGaugeDown {d : ℕ} (sig0 : ℝ) (X : HCPolySupport.BlockVec d) : HCPolySupport.BlockVec d

bfA_0^{-1/2} at the scalar bfA_0 = diag(sigma_0, sigma_0^{-1}).

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.blockGaugeDown sig0 X = ((√sig0)⁻¹ • X.1, √sig0 • X.2)

@[simp]

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.blockGaugeUp_fst {d : ℕ} (sig0 : ℝ) (X : HCPolySupport.BlockVec d) : (blockGaugeUp sig0 X).1 = √sig0 • X.1

@[simp]

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.blockGaugeUp_snd {d : ℕ} (sig0 : ℝ) (X : HCPolySupport.BlockVec d) : (blockGaugeUp sig0 X).2 = (√sig0)⁻¹ • X.2

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.blockVecDot_blockGaugeDown_blockGaugeUp {d : ℕ} {sig0 : ℝ} (hsig0 : 0 < sig0) (u F : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot (blockGaugeDown sig0 u) (blockGaugeUp sig0 F) = HCPolySupport.blockVecDot u F

The gauge conjugation identity. For a scalar bfA_0, conjugating the two sides of a block pairing by bfA_0^{\mp 1/2} leaves the pairing unchanged. This is the passage the manuscript performs between.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.blockVecDot_comm {d : ℕ} (X Y : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot X Y = HCPolySupport.blockVecDot Y X

blockVecDot is symmetric.

Fluctuations with vanishing cube average

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cubeAverageVec_cubeFluctuationVec {d : ℕ} (Q : HCPolySupport.TriadicCube d) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (hu : MeasureTheory.MemLp u 2 (HCPolySupport.normalizedCubeMeasure Q)) : HCPolySupport.cubeAverageVec Q (HCPolySupport.cubeFluctuationVec Q u) = 0

The cube average of a cube fluctuation vanishes.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cubeFluctuationVec_eq_self_of_cubeAverageVec_eq_zero {d : ℕ} (Q : HCPolySupport.TriadicCube d) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (hu : HCPolySupport.cubeAverageVec Q u = 0) : HCPolySupport.cubeFluctuationVec Q u = u

A field with vanishing cube average is its own fluctuation.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.blockCubeFluctuation_blockGaugeUp_eq_self {d : ℕ} (Q : HCPolySupport.TriadicCube d) (sig0 : ℝ) (F : HCPolySupport.Vec d → HCPolySupport.BlockVec d) (hzero1 : (HCPolySupport.cubeAverageVec Q fun (x : HCPolySupport.Vec d) => (F x).1) = 0) (hzero2 : (HCPolySupport.cubeAverageVec Q fun (x : HCPolySupport.Vec d) => (F x).2) = 0) : (blockCubeFluctuation Q fun (x : HCPolySupport.Vec d) => blockGaugeUp sig0 (F x)) = fun (x : HCPolySupport.Vec d) => blockGaugeUp sig0 (F x)

The gauged field of a mean-zero block field is its own doubled fluctuation.

The pinned duality constant and the gauged pairing bound

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.besovDualityConst {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) : ℝ

The duality constant, 2 d 3^{d+s} w(-s) w(s): the manuscript's generic C, made explicit.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.besovDualityConst Q s = 2 * ↑d * 3 ^ (↑d + s) * (HCPolySupport.cubeBesovScaleWeight (-s) Q * HCPolySupport.cubeBesovScaleWeight s Q)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.abs_cubeAverage_blockVecDot_le_besovDualityConst {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s sig0 : ℝ) (F Y : HCPolySupport.Vec d → HCPolySupport.BlockVec d) {Bu Bg : ℝ} (hs : 0 < s) (hsig0 : 0 < sig0) (hY1 : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => (Y x).1) 2 (HCPolySupport.normalizedCubeMeasure Q)) (hY2 : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => (Y x).2) 2 (HCPolySupport.normalizedCubeMeasure Q)) (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)) (hBg : 0 ≤ Bg) (hzero1 : (HCPolySupport.cubeAverageVec Q fun (x : HCPolySupport.Vec d) => (F x).1) = 0) (hzero2 : (HCPolySupport.cubeAverageVec Q fun (x : HCPolySupport.Vec d) => (F x).2) = 0) (hInt1 : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (blockGaugeDown sig0 (Y x)).1 (HCPolySupport.cubeFluctuationVec Q (fun (y : HCPolySupport.Vec d) => (blockGaugeUp sig0 (F y)).1) x)) (HCPolySupport.cubeSet Q) MeasureTheory.volume) (hInt2 : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (blockGaugeDown sig0 (Y x)).2 (HCPolySupport.cubeFluctuationVec Q (fun (y : HCPolySupport.Vec d) => (blockGaugeUp sig0 (F y)).2) x)) (HCPolySupport.cubeSet Q) MeasureTheory.volume) (hneg1 : ∀ (N : ℕ), (HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => (blockGaugeDown sig0 (Y x)).1) ≤ Bu) (hneg2 : ∀ (N : ℕ), (HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => (blockGaugeDown sig0 (Y x)).2) ≤ Bu) (hpos1 : ∀ (N : ℕ), (HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => (blockGaugeUp sig0 (F x)).1) ≤ Bg) (hpos2 : ∀ (N : ℕ), (HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => (blockGaugeUp sig0 (F x)).2) ≤ Bg) : |HCPolySupport.cubeAverage Q fun (x : HCPolySupport.Vec d) => HCPolySupport.blockVecDot (F x) (Y x)| ≤ besovDualityConst Q s * (Bu * Bg)

** with the gauge conjugation performed and the constant pinned.**

| fint_Q bfF_z . bfA_m tilde S_z |
  <= besovDualityConst Q s * ( Bu * Bg )

with Bu any envelope of the finite-depth negative q = 2 Besov seminorms of bfA_0^{-1/2} bfA_m tilde S_z and Bg any envelope of the finite-depth positive ones of bfA_0^{1/2} bfF_z.

: hs, hsig0, the four L^2 memberships, the two integrabilities and the four seminorm envelopes are caller obligations, discharged at the caller's carrier; hzero1, hzero2 are the cell mean-zeroness of e.Fz.def.