Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Provider.Regularity.StepSevenWireBridge

StepSevenWireBridge #

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

t.regularity Step 7d: the summability conversion B^{-1}_{2,1} ← B^{-t}_{2,2} #

The maneuver, on the proved carriers #

Both sides are already scale-normalized in CoarseGraining, with depth weight 3^{-s j} and the same depth average A_j = ⨍_{R ⊂ Q, depth j} |(F)_R|²:

  q = 1 at index 1 :  Σ_j 3^{-j}   √A_j          =  3^{-m}‖F‖_{B^{-1}_{2,1}(Q)}
  q = 2 at index t :  (Σ_j (3^{-tj}√A_j)²)^{1/2} =  3^{-tm}‖F‖_{B^{-t}_{2,2}(Q)}

Split the weight 3^{-j} = 3^{-(1-t)j}·3^{-tj} (depthSeminorm_one_eq), Cauchy--Schwarz the scale sum, and evaluate the geometric factor:

  Σ_j 3^{-j}√A_j  ≤  (Σ_j 3^{-2(1-t)j})^{1/2} · (Σ_j (3^{-tj}√A_j)²)^{1/2}
                  ≤  (1 - 3^{-2(1-t)})^{-1/2} · 3^{-tm}‖F‖_{B^{-t}_{2,2}(Q)} .

The 3^{-m} outer weight stays on the B^{-1}_{2,1} side and the 3^{-tm} on the B^{-t}_{2,2} side, because both CoarseGraining carriers put their whole scale dependence in the depth index j and none in the cube; no 3-power and no exponent moves anywhere.

What this discharges #

The scale-normalized bridge is the hbridge slot in CoarseGraining's carriers:

  scaleNormalizedNegativeBesovVectorNorm Q 1 (.finite 1) F
    ≤ Cbr(t) · scaleNormalizedNegativeBesovVectorNorm Q t (.finite 2) F ,

the left side being exactly what Algsuperdiff.Section3.Provider.Besov's embedding consumes (through cubeBesovNegativeVectorSeminorm, CoarseGraining's proved scaleNormalizedNegativeBesovVectorNorm_finite_one_eq_cubeBesovNegativeVectorSeminorm) and the right side exactly what coarsePoincareRHSTheory produces. hbridge is therefore no longer a conditional input.

References #

1. The geometric factor #

source
theorem Algsuperdiff.Section4.Provider.Regularity.geomPartialSum_le_inv {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (n : ℕ) :
∑ j ∈ Finset.range n, r ^ j ≤ (1 - r)⁻¹

The partial geometric sum is below its limit.

source
noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepSevenBridgeConst (t : ℝ) :
ℝ

The conversion constant (1 - 3^{-2(1-t)})^{-1/2}. At the §4.4 pin t = 1/4 it is (1 - 3^{-3/2})^{-1/2} ≈ 1.1128, absolute.

Equations
Instances For
    source
    theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenBridgeConst_nonneg (t : ℝ) :
    0 ≤ stepSevenBridgeConst t

    2. The weight split #

    source
    theorem Algsuperdiff.Section4.Provider.Regularity.depthSeminorm_one_eq {d : ℕ} (Q : HCPolySupport.TriadicCube d) (t : ℝ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (j : ℕ) :
    HCPolySupport.cubeBesovNegativeVectorDepthSeminorm Q 1 F j = Real.rpow 3 (-(1 - t)) ^ j * HCPolySupport.cubeBesovNegativeVectorDepthSeminorm Q t F j

    The scale-weight split: 3^{-j} = 3^{-(1-t)j}·3^{-tj} on the proved depth seminorms.

    3. The conversion at every finite depth #

    source
    theorem Algsuperdiff.Section4.Provider.Regularity.cubeBesovNegativeVectorPartialSeminorm_le_bridgeConst_mul {d : ℕ} (Q : HCPolySupport.TriadicCube d) {t : ℝ} (ht1 : t < 1) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (N : ℕ) :
    HCPolySupport.cubeBesovNegativeVectorPartialSeminorm Q 1 N F ≤ stepSevenBridgeConst t * HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q t N F

    The summability conversion, at every finite depth. The scale-sum Cauchy--Schwarz, with the geometric factor evaluated.

    4. hbridge, discharged #

    source
    theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenBesovBridge_of_partialBound {d : ℕ} (Q : HCPolySupport.TriadicCube d) {t : ℝ} (ht1 : t < 1) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) {B : ℝ} (hB : ∀ (N : ℕ), HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q t N F ≤ B) :
    HCPolySupport.cubeBesovNegativeVectorSeminorm Q 1 F ≤ stepSevenBridgeConst t * B

    hbridge from a uniform bound. Whenever B dominates every finite-depth B^{-t}_{2,2} partial seminorm of F, the note-normalized B^{-1}_{2,1} seminorm is at most C(t)·B.

    source
    theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenBesovBridge {d : ℕ} (Q : HCPolySupport.TriadicCube d) {t : ℝ} (ht1 : t < 1) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (hbdd : BddAbove (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q t N F)) :
    HCPolySupport.cubeBesovNegativeVectorSeminorm Q 1 F ≤ stepSevenBridgeConst t * HCPolySupport.cubeBesovNegativeVectorSeminormTwo Q t F