HomCGCarrierEnergy

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

The S-slot carrier comparison: the printed energy slot at BOTH spellings

What this file supplies

The obstruction was a single slot. The printed right-hand side of the general coarse-graining proposition carries the mesoscale energy

  ( Σ_{k ≤ n} 3^{-(s-s₁)p(n-k)} avsum_{z ∈ 3^k ℤ^d ∩ □_m}
        ‖σ^{1/2}∇u‖_{L²(z+□_k)}^p )^{1/p},

and the two transcriptions of that ONE object are

• CoarseGraining's weightedLocalSymmetricEnergyLp Q n hn a u s₁ s p — an ℝ≥0∞-valued tsum over ALL depths, with the per-cell energy given by localSymmetricEnergyENorm (the normalized ⟪∇u, 𝐚_sym ∇u⟫ integral);
• this repository's coarseGrainingEnergyPartial Q p (s-s₁) jn N Gen — a REAL-valued partial sum over the first N+1 depths, with the per-cell energy carried abstractly as Gen.

weightedLocalSymmetricEnergyLp_le_ofReal is the comparison in the direction the Step-4 consumption needs:

  (∀ N, coarseGrainingEnergyPartial Q p wgap jn N Gen ≤ S)  ⟹
      weightedLocalSymmetricEnergyLp Q n hn a u s₁ s p ≤ ENNReal.ofReal S,

whenever Gen dominates the printed per-cell energy printedLocalEnergy, (jn: ℤ) = Q.scale - n, and wgap ≤ s - s₁. The domination hypothesis is free: printedLocalEnergy is a DEFINITION (the CoarseGraining per-cell energy extended by 0 off the subcubes of Q), and localSymmetricEnergyENorm_le_ofReal_printedLocalEnergy proves the domination at Gen = printedLocalEnergy outright, because the CoarseGraining energy is finite (localSymmetricEnergyENorm_ne_top).

THE ORDER CONSTRAINT (load-bearing, recorded here)

The two spellings carry comparable geometric weights only when their order gaps do. CoarseGraining's series is weighted by 3^{-(s-s₁)pj} at ITS pair (s₁, s); this repository's by 3^{-wgap·p·i}. So the comparison needs wgap ≤ s - s₁ — the hypothesis hw below. Read at the spine's bundle, where this repository's gap is the s₁ = s/4 pin (wgap = 3s/4) and the display is entered at a LOWER order s′ with its own s₁′, this says

  s′ - s₁′  ≥  s - s/4 = 3s/4,

which forces s - s′ < s/4. The convenient choice s′ = s/2 is therefore NOT admissible for this route; s′ = 7s/8, s₁′ = s/8 is, and the smaller order loss s - s′ = s/8 only improves the duality window 0 < (s-s′)p′ < d.

1. The printed per-cell energy, as a total function on cubes

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.printedLocalEnergy {d : ℕ} {Q : HCPolySupport.TriadicCube d} (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain Q)) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) (R : HCPolySupport.TriadicCube d) : ℝ

The printed per-cell energy ‖σ^{1/2}∇u‖_{L²(R)}, as a total function of the cell R.

On a subcube of Q it is CoarseGraining's localSymmetricEnergyENorm of the restricted data; elsewhere it is 0. The dite is what turns the CoarseGraining summand — which is indexed by a MEMBERSHIP proof — into a function of the bare cube, so that it can sit in this repository's Gen slot.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.Homogenization.printedLocalEnergy_nonneg {d : ℕ} {Q : HCPolySupport.TriadicCube d} (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain Q)) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) (R : HCPolySupport.TriadicCube d) : 0 ≤ printedLocalEnergy a u R

theorem Algsuperdiff.Section4.Provider.Homogenization.localSymmetricEnergyENorm_le_ofReal_printedLocalEnergy {d : ℕ} {Q R : HCPolySupport.TriadicCube d} (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain Q)) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) (h : HCPolySupport.openCubeSet R ⊆ HCPolySupport.openCubeSet Q) : HCPolySupport.Book.Ch03.ABK26.localSymmetricEnergyENorm R (a.restrictToSubcube h) (HCPolySupport.Book.Ch03.ABK26.restrictH1ToSubcube u h) ≤ ENNReal.ofReal (printedLocalEnergy a u R)

The domination is free. The CoarseGraining per-cell energy is finite, so it is recovered exactly by ENNReal.ofReal of its own real value.

2. Two pieces of bookkeeping

3. THE CARRIER COMPARISON

theorem Algsuperdiff.Section4.Provider.Homogenization.weightedLocalSymmetricEnergyLp_le_ofReal {d : ℕ} {Q : HCPolySupport.TriadicCube d} {n : ℤ} (hn : n ≤ Q.scale) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain Q)) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) (s1 s : ↑HCPolySupport.FractionalOrder) (p : HCPolySupport.FiniteLpExponent) {wgap : ℝ} (hw : wgap ≤ ↑s - ↑s1) {jn : ℕ} (hjn : ↑jn = Q.scale - n) {Gen : HCPolySupport.TriadicCube d → ℝ} {S : ℝ} (hGen0 : ∀ (R : HCPolySupport.TriadicCube d), 0 ≤ Gen R) (hGen : ∀ (R : HCPolySupport.TriadicCube d), printedLocalEnergy a u R ≤ Gen R) (hS0 : 0 ≤ S) (hS : ∀ (N : ℕ), coarseGrainingEnergyPartial Q p.exponent.toReal wgap jn N Gen ≤ S) : HCPolySupport.Book.Ch03.ABK26.weightedLocalSymmetricEnergyLp Q n hn a u s1 s p ≤ ENNReal.ofReal S

The S-slot comparison, in the direction the Step-4 consumption needs.

If this repository's abstract per-cell datum Gen dominates the printed per-cell energy, and every partial ℓ^p sum of this repository's slot is below S, then CoarseGraining's tsum spelling of the SAME printed slot is below ENNReal.ofReal S.

The hypothesis hw is the order constraint recorded in the module docstring: the CoarseGraining pair (s₁, s) must have order gap at least this repository pair's wgap.