HomStepFourPairing #

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

Theorem B, §4.5, Step 4: the pairing carrier #

The object #

Step 4 uses the negative norm ‖·‖_{W_hat^{-s,∞}(□_m)} in exactly one way, the two duality pairings of the manuscript:

  |⨍_{□_m} ∇v · F|  ≤  ‖∇v‖_{W^{s,∞}(□_m)} ‖F‖_{W_hat^{-s,∞}(□_m)}.

The manuscript never defines W_hat^{-s,p} (the manuscript defines only the order -1 duals, and it defines those by duality: a supremum of ∫_U f g over a normalized test class). Following that pattern — and the corrected rendering of the same symbol — the carrier here is the duality form: WeakNegDualBoundOn Q s W F is the family of pairing inequalities. The Step-4 pairing is then a theorem (WeakNegDualBoundOn.pairing) rather than an assumption.

The test gauge #

wsInftyGauge Q s Ksup KHol = 3^{-s·Q.scale} · Ksup + KHol is the printed display's volume-normalized Hölder norm ‖φ‖_{C^{0,s}(□_m)} = |□_m|^{-s/d}‖φ‖_{L^∞} + [φ]_{C^{0,s}}, which the manuscript declares interchangeable with ‖·‖_{W^{s,∞}(□_m)} up to dimensional constants. Both halves are carried: The manuscript's Step-4 test function is ∇v, whose mean does not vanish, so the L^∞ half is load-bearing (see the disclosure below).

Two inequivalent renderings of one printed symbol #

The §4.5 negative-norm symbol is consumed at two sites that demand inequivalent objects:

Step 3c (the L^∞ upgrade) needs the multiscale reading — a bound on the cube averages of F at every scale (this file's negBesovInftyNorm, this file's UniformBoxGaugeBound). A single-scale duality bound does not give it: it loses r^{-d} (machine-checked).
Step 4 (here) needs the duality reading. The multiscale reading does not give it either: pairing B^{s}_{∞,∞} against B^{-s}_{∞,∞} diverges logarithmically in the number of scales (the increments contribute a constant per scale).

Neither implies the other. Both are legitimate readings of an undefined printed symbol; each Step consumes the one it needs, and each is disclosed at its own consumption site.

The hat #

The printed display's W_hat^{-1,p'} restricts the test class to mean-zero g. Under the hatted reading the pairing above is valid only for mean-zero φ; the general φ splits as φ = (φ)_{□_m} + (φ - (φ)_{□_m}) and the constant part pairs against ⨍_{□_m} F. weakNegDual_of_hat_of_mean_zero records the case in which the two coincide — ⨍_{□_m} F = 0, which is exactly the gradient leg F = ∇u - ∇v with u - v ∈ H¹₀(□_m). For the flux leg F = a_L∇u - σ_m∇v the mean does not vanish and is not controlled by the hatted norm; that is the second half of the correction draft.

1. The pairing functional #

source

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.cubePairing {d : ℕ} (Q : HCPolySupport.TriadicCube d) (F phi : HCPolySupport.Vec d → HCPolySupport.Vec d) :

ℝ

⨍_{□} F · φ, the volume-normalized pairing of two vector fields on the open realization of a triadic cube.

Equations

Algsuperdiff.Section4.Provider.Homogenization.cubePairing Q F phi = HCPolySupport.volumeAverage (HCPolySupport.openCubeSet Q) fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (F x) (phi x)

Instances For

source

theorem Algsuperdiff.Section4.Provider.Homogenization.cubePairing_def {d : ℕ} (Q : HCPolySupport.TriadicCube d) (F phi : HCPolySupport.Vec d → HCPolySupport.Vec d) :

cubePairing Q F phi = HCPolySupport.volumeAverage (HCPolySupport.openCubeSet Q) fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (F x) (phi x)

2. The test gauge `‖φ‖_{W^{s,∞}(□_m)}` #

source

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.wsInftyGauge {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s Ksup KHol : ℝ) :

ℝ

the printed display's volume-normalized Hölder norm on □_m, 3^{-s·m}‖φ‖_{L^∞(□_m)} + [φ]_{C^{0,s}(□_m)}, presented at the two explicit data Ksup and KHol rather than as a constructed norm.

Equations

Algsuperdiff.Section4.Provider.Homogenization.wsInftyGauge Q s Ksup KHol = Real.rpow 3 (-(s * ↑Q.scale)) * Ksup + KHol

Instances For

source

theorem Algsuperdiff.Section4.Provider.Homogenization.wsInftyGauge_def {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s Ksup KHol : ℝ) :

wsInftyGauge Q s Ksup KHol = Real.rpow 3 (-(s * ↑Q.scale)) * Ksup + KHol

source

theorem Algsuperdiff.Section4.Provider.Homogenization.wsInftyGauge_nonneg {d : ℕ} {Q : HCPolySupport.TriadicCube d} {s Ksup KHol : ℝ} (hs : 0 ≤ Ksup) (hk : 0 ≤ KHol) :

0 ≤ wsInftyGauge Q s Ksup KHol

3. The duality-form negative gauge #

source

def Algsuperdiff.Section4.Provider.Homogenization.WeakNegDualBoundOn {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s W : ℝ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) :

Prop

‖F‖_{W_hat^{-s,∞}(□_m)} ≤ W, in duality form (a correction to the printed statement).

The predicate is the family of pairing inequalities the manuscript uses: for every test field φ with volume-normalized Hölder norm at most wsInftyGauge Q s Ksup KHol,

  |⨍_{□} F · φ| ≤ W · (3^{-s·m} Ksup + KHol).

This is the printed display's own definitional pattern for the negative-order duals, transported from order -1 to order -s. CoarseGraining's cubeEuclideanNegativeWspSmoothDualENorm (Homogenization/Sobolev/Fractional/EuclideanWspSmoothDual.lean) is the same construction at a bundled L² carrier and smooth tests; the lightweight predicate here is the one the §4.5 consumers need.

Equations