Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Provider.Homogenization.HomCGDischargeBridge

HomCGDischargeBridge #

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

The middle link: descendant smooth duals from descendant negative Besov data #

What this file is for #

The printed finite-p coarse-graining display is a composition of three CoarseGraining statements:

  (1)  exists_centeredCubeFluxComparison_cz          -- the printed LHS pair
  (2)  the smooth-dual / negative-Besov comparison   -- the middle link
  (3)  exists_localCoarseGrainingLp                  -- the printed RHS

Link (1) speaks about the smooth-dual ℓ^p descendant average of the local flux defect; link (3) bounds the negative-Besov ℓ^p descendant average of the same defect fields. The two averages are different objects, and (2) is the only thing that joins them. This file performs that join once, at the exact carriers of (1) and (3):

The 3^{s n} is not a loss: it is exactly the normalization 3^{-s n} that CoarseGraining's localFluxDefectNegativeBesovLpAverage carries in front and the smooth-dual average does not. Composed with the 3^{s(m-n)} of link (1) it produces the printed 3^{s m}, i.e. the printed 3^{-ms} on the left.

The per-descendant identification #

The two links name the same field by two different constructors: centeredCubeLocalFluxDefectL2Field (link 1) and localFluxDefectL2Field (link 3). Both carry x ↦ (𝐚(x) - σ₀ I)∇u(x) and differ only in the Prop certificate, so they are definitionally equal — recorded here as centeredCubeLocalFluxDefectL2Field_eq.

1. The two constructors of the local flux defect agree #

source
theorem Algsuperdiff.Section4.Provider.Homogenization.centeredCubeLocalFluxDefectL2Field_eq {d : ℕ} {m n : ℤ} (hnm : n < m) (hn : n ≤ (HCPolySupport.originCube d m).scale) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d m))) (sigma0 : ℝ) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (R : HCPolySupport.TriadicCube d) (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) n) :
HCPolySupport.Book.Ch03.ABK26.centeredCubeLocalFluxDefectL2Field m n hnm a sigma0 u R hR = HCPolySupport.Book.Ch03.ABK26.localFluxDefectL2Field a ⋯ sigma0 u

The flux-defect fields of the two CoarseGraining links are the same field.

centeredCubeLocalFluxDefectL2Field (the flux-comparison side) and localFluxDefectL2Field (the coarse-graining side) have the same toField, x ↦ (𝐚(x) - σ₀ I)∇u(x), and differ only in their MemLp certificate.

2. The exponent of a finite L^p index is a positive real #

source
theorem Algsuperdiff.Section4.Provider.Homogenization.finiteLpExponent_toReal_pos (p : HCPolySupport.FiniteLpExponent) :
0 < p.exponent.toReal

The real exponent attached to a FiniteLpExponent is positive.

source
theorem Algsuperdiff.Section4.Provider.Homogenization.localFluxDefect_smoothDualAverage_le {d : ℕ} {m n : ℤ} (hnm : n < m) (hn : n ≤ (HCPolySupport.originCube d m).scale) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d m))) (sigma0 : ℝ) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (s : ↑HCPolySupport.FractionalOrder) (p : HCPolySupport.FiniteLpExponent) :
HCPolySupport.Book.Ch03.ABK26.centeredCubeLocalFluxDefectSmoothDualLpAverage m n hnm a sigma0 u s p ≤ HCPolySupport.cubeEuclideanNegativeWspSmoothDualBesovConstant d * ENNReal.ofReal (Real.rpow 3 (↑s * ↑n)) * HCPolySupport.Book.Ch03.ABK26.localFluxDefectNegativeBesovLpAverage (HCPolySupport.originCube d m) n hn a sigma0 u s p

The descendant smooth-dual average is controlled by the descendant negative-Besov average.

This is the comparison cubeEuclideanNegativeWspSmoothDualENorm_le_cubeEuclideanNegativeBesovESeminorm applied on every descendant, aggregated through the ℓ^p average, and renormalized by the 3^{-s n} that CoarseGraining's negative-Besov average carries.