PrincipalResponseLegsBudgetEllipticity

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

Provider: sub-step (ii) of the principal response, the ellipticity budget

Source display, immediately preceding the independence sentence:

avsum_{z in 3^n Zd cap cu_K}
  E[ shom_{m-h} |p_z|^2 + shom_{m-h}^{-1} |q_z|^2 ] <= C ,

quoted from e.nablaw.in.L.eight (label). Here (p_z; q_z) = P_z is the localized load of e.Pz.def (label), carried in this repository by principalPz with components principalPz_fst and principalPz_snd.

What this module proves

Because P_z is by definition bfAhom_{m-h}^{-1/2} applied to the raw averaged slope pair, the two normalizations cancel exactly against the two weights shom_{m-h} and shom_{m-h}^{-1} of the display. The integrand is therefore an unnormalized quantity:

• ellipticityBudget_eq -- the exact collapse

  shom |p_z|^2 + shom^{-1}|q_z|^2
    = |e' + (grad w_D)_R|^2 + |e + (grad w_N + shom^{-1} h e')_R|^2 ,
  

  an unconditional identity, with R the localization cube.

The per-cube Jensen step, the grid average over the triadic subcubes of cu_K at the localization scale, and the passage to expectations all belong to the consuming lane. Carried out there, this identity gives the manuscript's left-hand side bounded by 2(|e|^2 + |e'|^2) + 2 E[ ‖grad w_D‖^2_{L^2(cu_K)} ] + 2 E[ ‖grad w_N + shom^{-1} h e'‖^2_{L^2(cu_K)} ], which is what e.nablaw.in.L.eight is quoted for.

The grid rendering

The source averages over the lattice 3^n Zd cap cu_K, i.e. over the cubes `z

• cu_ntilingcu_K. Those cubes are exactly the triadic descendants of cu_Kat depthK - n, and the repository's descendantsAverageis the corresponding average; this is the standard rendering used throughout `Provider/BadEvents` and elsewhere in this tree.

The collapse of the two normalizations

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.ellipticityBudget_eq {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} (R : HCPolySupport.TriadicCube d) (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) : ↑sigma * HCPolySupport.vecNormSq (principalPz sigma omega lowScale highScale e e' R wD wN).1 + (↑sigma)⁻¹ * HCPolySupport.vecNormSq (principalPz sigma omega lowScale highScale e e' R wD wN).2 = HCPolySupport.vecNormSq (e' + HCPolySupport.cubeAverageVec R fun (x : HCPolySupport.Vec d) => wD.grad x) + HCPolySupport.vecNormSq (e + HCPolySupport.cubeAverageVec R (neumannFluxField sigma omega lowScale highScale e' wN))

The integrand, collapsed. The weights shom_{m-h} and shom_{m-h}^{-1} cancel the two legs of the normalization bfAhom_{m-h}^{-1/2} in e.Pz.def exactly, leaving the squared lengths of the raw averaged slope pair.