LocalizedTranslation

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

Translation covariance of the localized quantities

The localized error and regularity on a cube centred at y agree with their origin-centred versions after translating the cutoff sample by y. Translation invariance of the cutoff-sample law then makes every measurable moment of these quantities independent of the centre.

theorem Algsuperdiff.Section5.Support.cubeSetAt_zero {d : ℕ} (n : ℤ) : cubeSetAt 0 n = HCPolySupport.openCubeSet (HCPolySupport.originCube d n)

noncomputable def Algsuperdiff.Section5.Support.toOriginWitness {d : ℕ} (n : ℤ) (y : HCPolySupport.Vec d) (u : HCPolySupport.H1Function (cubeSetAt y n)) : HCPolySupport.H1Function (cubeSetAt 0 n)

Pull a Sobolev witness on a translated cube back to the cube at the origin.

Equations

• Algsuperdiff.Section5.Support.toOriginWitness n y u = Algsuperdiff.Section5.Support.castH1 ⋯ (Algsuperdiff.Section5.Support.originPullback y n u)

noncomputable def Algsuperdiff.Section5.Support.fromOriginWitness {d : ℕ} (n : ℤ) (y : HCPolySupport.Vec d) (u : HCPolySupport.H1Function (cubeSetAt 0 n)) : HCPolySupport.H1Function (cubeSetAt y n)

Translate a Sobolev witness from the origin cube to the specified cube.

Equations

• Algsuperdiff.Section5.Support.fromOriginWitness n y u = Algsuperdiff.Section5.Support.translateSolution y n (Algsuperdiff.Section5.Support.castH1 ⋯ u)

theorem Algsuperdiff.Section5.Support.localizedError_eq_translateCutoffSample {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) : localizedError M n y omega = localizedError M n 0 (Section3.Cutoff.translateCutoffSample y omega)

The localized error at y + □_n is the origin value of the translated sample.

Moment identities

theorem Algsuperdiff.Section5.Support.lintegral_localizedError_rpow_eq_origin {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) (p : ℝ) : ∫⁻ (omega : Section3.Cutoff.CutoffSample d), localizedError M n y omega ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) = ∫⁻ (omega : Section3.Cutoff.CutoffSample d), localizedError M n 0 omega ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M)

Every real-power moment of the localized error is independent of the cube centre.