CoarseDirichletEnergy #

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

The Dirichlet energy right-hand side at the pin `r = s/2` #

Nothing here claims the anchor or any source node.

What is proved #

CoarseGraining's dirichletEnergyWithRHSRHS — the right-hand side of the general-data energy estimate, which BoundaryEnergyRebase puts on the covering cube — read at the fidelity plan's pin r = s/2 and priced onto the frozen clause's own legs:

  dirichletEnergyWithRHSRHS C (□_{n+2}) ã (s/2) (−g(·+c)) v
      ≤ C (s/2)^{-3/2} √K √(σ_{n+3}^{-1}) · C_bg 3^{s(n+2)} C_gw [g]_{H^s(W')}
      + C (s/2)^{-1/2} √K √(σ_{n+3})
            · ( √d 3^d ‖∇h‖_{L²(W')} + C_bg 3^{s(n+2)} C_gw [∇h]_{H^s(W')} ) .

The three legs on the right are the frozen clause's own [g], ‖∇h‖_{L²} and [∇h]_{H^s} legs, at the exact shapes the CoarseAssemblyBudget regrouping consumes.

Ingredients, all proved:

the two q = 2 ellipticity caps at the pin's indices s/2 and s/4 (CoarseIndexBridges.ae_coveringCubeRatioCap_le);
the positive-Besov index conversion [·]_{s/2} → [·]_s (CoarseIndexBridges; constant-free);
the force window transport (BoundaryTransports.besovVectorSeminormTwo_coveringCube_le_anchorWindow);
the two ∇h conversions (BoundaryGradH.besovVectorSeminormTwo_datumGrad_coveringCube_le_anchorWindow and ...sqrt_vecNormSq_cubeAverageVec_coveringCube_le_anchorWindow).

References #

CoarseGraining, dirichletEnergyWithRHSRHS.

1. The two capped ellipticity factors #

source

theorem Algsuperdiff.Section4.Provider.ExcessDecay.rpow_neg_half_le_of_lower_cap {l sigma K : ℝ} (hl : 0 ≤ l) (hsigma : 0 < sigma) (hK : 0 ≤ K) (hcap : sigma * l⁻¹ ≤ K) :

l.rpow (-(1 / 2)) ≤ √K * √sigma⁻¹

The lower ellipticity factor λ^{-1/2} from the q = 2 ratio cap.

source

theorem Algsuperdiff.Section4.Provider.ExcessDecay.rpow_half_le_of_upper_cap {Lam sigma K : ℝ} (hLam : 0 ≤ Lam) (hsigma : 0 < sigma) (hcap : sigma⁻¹ * Lam ≤ K) :

Lam.rpow (1 / 2) ≤ √K * √sigma

The upper ellipticity factor Λ^{1/2} from the q = 2 ratio cap.

2. The Dirichlet energy right-hand side, priced #

source

HCPolySupport.Book.Ch03.dirichletEnergyWithRHSRHS C₂ (HCPolySupport.originCube d (n + 2)) a (s / 2) (fun (y : HCPolySupport.Vec d) => -g (y + c)) v ≤ C₂ * (s / 2).rpow (-(3 / 2)) * (√K * √sigma⁻¹) * (besovGagliardoConstant d * Real.rpow 3 (s * ↑(n + 2)) * (gagliardoWindowConst d * (Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s g).toReal)) + C₂ * (s / 2).rpow (-(1 / 2)) * (√K * √sigma) * (√↑d * 3 ^ d * (MeasureTheory.eLpNorm hdat.grad 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal + besovGagliardoConstant d * Real.rpow 3 (s * ↑(n + 2)) * (gagliardoWindowConst d * (Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s hdat.grad).toReal))

Dirichlet energy bound from covering-cube containment in the anchor window.

source

CoarseGraining's dirichletEnergyWithRHSRHS on the boundary covering cube at the pin r = s/2, priced onto the frozen clause's three legs.

hlam and hLam are the two q = 2 ratio caps of CoarseIndexBridges.ae_coveringCubeRatioCap_le at the indices s/4 and s/2; hvgrad is the boundary-gradient identity carried by the produced Dirichlet comparison of BoundaryEnergyRebase.

Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Provider.ExcessDecay.CoarseDirichletEnergy

CoarseDirichletEnergy #

The Dirichlet energy right-hand side at the pin `r = s/2` #

What is proved #

References #

1. The two capped ellipticity factors #

2. The Dirichlet energy right-hand side, priced #

CoarseDirichletEnergy #

The Dirichlet energy right-hand side at the pin r = s/2 #

What is proved #

References #

1. The two capped ellipticity factors #

2. The Dirichlet energy right-hand side, priced #

The Dirichlet energy right-hand side at the pin `r = s/2` #