HomCGCarrierRHS

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

The printed right-hand side at both spellings

What this file supplies

The measurement was that CoarseGraining's localCoarseGrainingLpRHS and this repository's coarseGrainingFinitePRHS "match term for term", with the ONE real issue at the S-slot. HomCGCarrierEnergy settles the S-slot; this file performs the remaining, purely bookkeeping half:

  localCoarseGrainingLpRHS C Q n hn 𝐚 σ₀ hσ₀ 𝐠 u s₁ s s₂ p
      ≤ ENNReal.ofReal (coarseGrainingFinitePRHS Ccg s s₂ σ₀ E₁ E₂ D_g S n)

as soon as the four abstract slots of this repository's spelling dominate the four printed carriers of CoarseGraining's:

repo slot	printed carrier
Ccg	the produced constant C(p,d)
E₁	parentTruncatedHomogenizationErrorInfinityOneScalar … s₁
E₂	parentTruncatedHomogenizationErrorInfinityTwoScalar … (s₁/2)
D_g	cubeEuclideanPositiveBesovOverlapESeminorm □_m s₂ p 𝐠
S	weightedLocalSymmetricEnergyLp (HomCGCarrierEnergy)

Everything else is an ℝ≥0∞/ℝ transfer of the printed scalars: s^{-1}, σ₀^{1/2} = √σ₀, s^{-9/2}, (s₂-s)^{-1}, 1 + E₂² and 3^{s₂n}. Every transfer is an EQUALITY, so no constant is lost here.

The order slot is NOT transferred here

The display is entered at the order s′ the carrier comparison forces (see HomCGCarrierEnergy), so the right-hand side below is the printed one READ AT s′: its prefactors are s′^{-1}, s′^{-9/2} and (s₂-s′)^{-1}. No transfer back to the data order s is attempted, and none is needed: the Step-4 consumption site takes its own arithmetic side condition at its own order, exactly as the per-site disposition of the corrected reading.

1. The right-hand side, transferred

theorem Algsuperdiff.Section4.Provider.Homogenization.localCoarseGrainingLpRHS_le_ofReal {d : ℕ} {Q : HCPolySupport.TriadicCube d} {n : ℤ} (hn : n ≤ Q.scale) {C : ENNReal} (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain Q)) {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) (s1 s s2 : ↑HCPolySupport.FractionalOrder) (p : HCPolySupport.FiniteLpExponent) (hss2 : ↑s < ↑s2) {Ccg E1 E2 Dg S : ℝ} (hCcg0 : 0 ≤ Ccg) (hE10 : 0 ≤ E1) (hE20 : 0 ≤ E2) (hDg0 : 0 ≤ Dg) (hS0 : 0 ≤ S) (hC : C ≤ ENNReal.ofReal Ccg) (hE1 : HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityOneScalar Q n hn a sigma0 hsigma0 s1 ≤ ENNReal.ofReal E1) (hE2 : HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityTwoScalar Q n hn a sigma0 hsigma0 (HCPolySupport.fractionalOrderHalf s1) ≤ ENNReal.ofReal E2) (hDg : HCPolySupport.Book.Ch03.ABK26.cubeEuclideanPositiveBesovOverlapESeminorm Q s2 p g ≤ ENNReal.ofReal Dg) (hSlot : HCPolySupport.Book.Ch03.ABK26.weightedLocalSymmetricEnergyLp Q n hn a u s1 s p ≤ ENNReal.ofReal S) : HCPolySupport.Book.Ch03.ABK26.localCoarseGrainingLpRHS C Q n hn a sigma0 hsigma0 g u s1 s s2 p ≤ ENNReal.ofReal (coarseGrainingFinitePRHS Ccg (↑s) (↑s2) sigma0 E1 E2 Dg S n)

The printed right-hand side, at this repository's real-valued spelling.

2. Nonnegativity of the transferred right-hand side

theorem Algsuperdiff.Section4.Provider.Homogenization.coarseGrainingFinitePRHS_nonneg {Ccg s s2 sigma E1 E2 Dg S : ℝ} {n : ℤ} (hCcg0 : 0 ≤ Ccg) (hs0 : 0 < s) (hss2 : s < s2) (hE10 : 0 ≤ E1) (hE20 : 0 ≤ E2) (hDg0 : 0 ≤ Dg) (hS0 : 0 ≤ S) : 0 ≤ coarseGrainingFinitePRHS Ccg s s2 sigma E1 E2 Dg S n

This repository's spelling of the printed right-hand side is nonnegative on the printed data.

theorem Algsuperdiff.Section4.Provider.Homogenization.localCoarseGrainingLpRHS_toReal_le {d : ℕ} {Q : HCPolySupport.TriadicCube d} {n : ℤ} (hn : n ≤ Q.scale) {C : ENNReal} (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain Q)) {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) (s1 s s2 : ↑HCPolySupport.FractionalOrder) (p : HCPolySupport.FiniteLpExponent) (hss2 : ↑s < ↑s2) {Ccg E1 E2 Dg S : ℝ} (hCcg0 : 0 ≤ Ccg) (hE10 : 0 ≤ E1) (hE20 : 0 ≤ E2) (hDg0 : 0 ≤ Dg) (hS0 : 0 ≤ S) (hC : C ≤ ENNReal.ofReal Ccg) (hE1 : HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityOneScalar Q n hn a sigma0 hsigma0 s1 ≤ ENNReal.ofReal E1) (hE2 : HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityTwoScalar Q n hn a sigma0 hsigma0 (HCPolySupport.fractionalOrderHalf s1) ≤ ENNReal.ofReal E2) (hDg : HCPolySupport.Book.Ch03.ABK26.cubeEuclideanPositiveBesovOverlapESeminorm Q s2 p g ≤ ENNReal.ofReal Dg) (hSlot : HCPolySupport.Book.Ch03.ABK26.weightedLocalSymmetricEnergyLp Q n hn a u s1 s p ≤ ENNReal.ofReal S) : (HCPolySupport.Book.Ch03.ABK26.localCoarseGrainingLpRHS C Q n hn a sigma0 hsigma0 g u s1 s s2 p).toReal ≤ coarseGrainingFinitePRHS Ccg (↑s) (↑s2) sigma0 E1 E2 Dg S n

The real value of the printed right-hand side, from the transferred bound.

theorem Algsuperdiff.Section4.Provider.Homogenization.localCoarseGrainingLpRHS_ne_top {d : ℕ} {Q : HCPolySupport.TriadicCube d} {n : ℤ} (hn : n ≤ Q.scale) {C : ENNReal} (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain Q)) {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) (s1 s s2 : ↑HCPolySupport.FractionalOrder) (p : HCPolySupport.FiniteLpExponent) (hss2 : ↑s < ↑s2) {Ccg E1 E2 Dg S : ℝ} (hCcg0 : 0 ≤ Ccg) (hE10 : 0 ≤ E1) (hE20 : 0 ≤ E2) (hDg0 : 0 ≤ Dg) (hS0 : 0 ≤ S) (hC : C ≤ ENNReal.ofReal Ccg) (hE1 : HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityOneScalar Q n hn a sigma0 hsigma0 s1 ≤ ENNReal.ofReal E1) (hE2 : HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityTwoScalar Q n hn a sigma0 hsigma0 (HCPolySupport.fractionalOrderHalf s1) ≤ ENNReal.ofReal E2) (hDg : HCPolySupport.Book.Ch03.ABK26.cubeEuclideanPositiveBesovOverlapESeminorm Q s2 p g ≤ ENNReal.ofReal Dg) (hSlot : HCPolySupport.Book.Ch03.ABK26.weightedLocalSymmetricEnergyLp Q n hn a u s1 s p ≤ ENNReal.ofReal S) : HCPolySupport.Book.Ch03.ABK26.localCoarseGrainingLpRHS C Q n hn a sigma0 hsigma0 g u s1 s s2 p ≠ ⊤

The transferred right-hand side is finite.