InteriorEnergyBridge

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

The energy leg of the interior clause: child frame versus parent frame

The coarse-graining energy term of the child-frame composition carries CoarseGraining's coefficient-energy norm at the child's own frame,

  ‖∇u_tilde_x‖_{ã, L²(□_n)}  =  h1EnergyNormOnCube □_n ã u_tilde_x ,   u_tilde_x = u(· + x) ,

  localizedCoeffEnergyValue ((x−z) + □_n) ã_{L,n+2} u_tilde_z ,       u_tilde_z = u(· + z) .

The two agree exactly. Two facts, both identities:

• the flux increment is antisymmetric, so the quadratic form of the shifted coefficient is the quadratic form of a_L, i.e. exactly ν |ξ|² (AntisymmetricShiftCutoff.vecDot_matVecMul_fluxCorrectedField_self, NuIdentification); the same is true of the re-based family, whose subtracted constant is the parent's increment. So both sides are ν ⨍ |∇u|² on their own window;
• only the volume average has to move, and Lebesgue measure is translation invariant (TranslationTransportNorms), so ⨍_{(x−z)+□_n} |∇u(·+z)|² is ⨍_{□_n} |∇u(·+x)|².

No constant, no hypothesis, no good event.

References

• ABK26, (the ν|∇u|² energy reading).

1. The ν-identification at the re-based family

theorem Algsuperdiff.Section4.Provider.ExcessDecay.symmPart_parentRebasedFamily {d : ℕ} (M : Section3.ABKModel d) (L k : ℤ) (x z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) (Q : HCPolySupport.TriadicCube d) (y : HCPolySupport.Vec d) : HCPolySupport.symmPart (((parentRebasedFamily M L k x z omega).coeffOn Q).toCoeffField y) = M.nu • 1

The symmetric part of the re-based child-frame coefficient is exactly ν Id: the subtracted constant is the parent's antisymmetric increment.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.localizedCoeffEnergyValue_parentRebasedFamily_eq {d : ℕ} (M : Section3.ABKModel d) (L k : ℤ) (x z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) (Q : HCPolySupport.TriadicCube d) (V : Set (HCPolySupport.Vec d)) (u : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier) : HCPolySupport.Book.Ch03.localizedCoeffEnergyValue V ((parentRebasedFamily M L k x z omega).coeffOn Q) u = M.nu * HCPolySupport.Book.Ch03.normalizedSetAverage V fun (y : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (u.grad y)

The ν-identification at the re-based family. On any window, the localized coefficient energy is exactly ν times the normalized gradient L² square.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.h1EnergyNormOnCube_parentRebasedFamily_eq {d : ℕ} (M : Section3.ABKModel d) (L k n : ℤ) (x z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) (u : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d n)).carrier) : HCPolySupport.Book.Ch03.h1EnergyNormOnCube (HCPolySupport.originCube d n) (parentRebasedFamily M L k x z omega) u = √(M.nu * HCPolySupport.Book.Ch03.normalizedSetAverage (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (y : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (u.grad y))

The coefficient-energy norm of the re-based family on the child cube.

2. The volume average moves

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedSetAverage_vecNormSq_grad_frame {d : ℕ} (n : ℤ) (x z : HCPolySupport.Vec d) (G : HCPolySupport.Vec d → HCPolySupport.Vec d) : (HCPolySupport.Book.Ch03.normalizedSetAverage ((fun (y : HCPolySupport.Vec d) => x - z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (y : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (G (y + z))) = HCPolySupport.Book.Ch03.normalizedSetAverage (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (y : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (G (y + x))

The gradient energy average transports between the two frames.

The normalized average of |∇u(· + z)|² over (x−z) + □_n is the normalized average of |∇u(· + x)|² over □_n. Exact.

3. The energy leg

theorem Algsuperdiff.Section4.Provider.ExcessDecay.h1EnergyNormOnCube_parentRebasedFamily_eq_sqrt_localizedCoeffEnergyValue {d : ℕ} {n m k : ℤ} (M : Section3.ABKModel d) (L : ℤ) (x z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (hx : HCPolySupport.translateSet x (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hz : HCPolySupport.translateSet z (HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) : HCPolySupport.Book.Ch03.h1EnergyNormOnCube (HCPolySupport.originCube d n) (parentRebasedFamily M L k x z omega) (HCPolySupport.H1Function.untranslate x (u.restrict ⋯ hx)) = √(HCPolySupport.Book.Ch03.localizedCoeffEnergyValue ((fun (y : HCPolySupport.Vec d) => x - z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) ((Support.fluxCorrectedCoeffFamily M L k (HCPolySupport.originCube d k) (Section3.Cutoff.translateCutoffSample z omega)).coeffOn (HCPolySupport.originCube d k)) (HCPolySupport.H1Function.untranslate z (u.restrict ⋯ hz)))

The energy leg of the interior clause.

  ‖∇u_tilde_x‖_{ã, L²(□_n)}  =  ( ⨍_{(x−z)+□_n} ∇u_tilde_z · ã_{L,n+2} ∇u_tilde_z )^{1/2} .