Coarse-graining support: Support.Sobolev.Fractional.EuclideanWsp

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Euclidean fractional Sobolev core

The exact Chapter 3 Euclidean W^(s,p) kernel and full power norm on a triadic cube.

noncomputable def HCPolySupport.cubeEuclideanWspKernel {d : ℕ} (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) : Vec d × Vec d → HilbertVec d

The Hilbert-vector difference kernel (F(x) - F(y)) / |x - y|^(s + d/p) using Euclidean distance.

Equations

• HCPolySupport.cubeEuclideanWspKernel s p F z = HCPolySupport.euclideanDist z.1 z.2 ^ (-(↑s + ↑d / p.exponent.toReal)) • HCPolySupport.HilbertVec.ofVec (F z.1 - F z.2)

@[simp]

theorem HCPolySupport.cubeEuclideanWspKernel_apply {d : ℕ} (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) (z : Vec d × Vec d) : cubeEuclideanWspKernel s p F z = euclideanDist z.1 z.2 ^ (-(↑s + ↑d / p.exponent.toReal)) • HilbertVec.ofVec (F z.1 - F z.2)

theorem HCPolySupport.norm_cubeEuclideanWspKernel {d : ℕ} (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) (z : Vec d × Vec d) : ‖cubeEuclideanWspKernel s p F z‖ = euclideanDist z.1 z.2 ^ (-(↑s + ↑d / p.exponent.toReal)) * euclideanNorm (F z.1 - F z.2)

def HCPolySupport.MemCubeEuclideanWsp {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) : Prop

The Euclidean fractional difference kernel of F belongs to Lᵖ for the cube Gagliardo pair measure.

Equations

• HCPolySupport.MemCubeEuclideanWsp Q s p F = MeasureTheory.MemLp (HCPolySupport.cubeEuclideanWspKernel s p F) p.exponent (HCPolySupport.Gagliardo.gagliardoCubeMeasure Q)

noncomputable def HCPolySupport.cubeEuclideanWspESeminorm {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) : ENNReal

The extended Lᵖ norm of the Euclidean fractional difference kernel for the cube Gagliardo pair measure.

Equations

• HCPolySupport.cubeEuclideanWspESeminorm Q s p F = MeasureTheory.eLpNorm (HCPolySupport.cubeEuclideanWspKernel s p F) p.exponent (HCPolySupport.Gagliardo.gagliardoCubeMeasure Q)

theorem HCPolySupport.cubeEuclideanWspESeminorm_eq_lintegral {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) (hF : MeasureTheory.AEStronglyMeasurable (cubeEuclideanWspKernel s p F) (Gagliardo.gagliardoCubeMeasure Q)) : cubeEuclideanWspESeminorm Q s p F = (∫⁻ (z : Vec d × Vec d), ‖cubeEuclideanWspKernel s p F z‖ₑ ^ p.exponent.toReal ∂Gagliardo.gagliardoCubeMeasure Q) ^ (1 / p.exponent.toReal)

theorem HCPolySupport.memCubeEuclideanWsp_iff {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} {F : Vec d → Vec d} : MemCubeEuclideanWsp Q s p F ↔ MeasureTheory.AEStronglyMeasurable (cubeEuclideanWspKernel s p F) (Gagliardo.gagliardoCubeMeasure Q) ∧ cubeEuclideanWspESeminorm Q s p F < ⊤

theorem HCPolySupport.MemCubeEuclideanWsp.aestronglyMeasurable {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} {F : Vec d → Vec d} (hF : MemCubeEuclideanWsp Q s p F) : MeasureTheory.AEStronglyMeasurable (cubeEuclideanWspKernel s p F) (Gagliardo.gagliardoCubeMeasure Q)

theorem HCPolySupport.MemCubeEuclideanWsp.eSeminorm_lt_top {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} {F : Vec d → Vec d} (hF : MemCubeEuclideanWsp Q s p F) : cubeEuclideanWspESeminorm Q s p F < ⊤

structure HCPolySupport.CubeEuclideanWspField {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) extends HCPolySupport.CubeEuclideanLpField Q p : Type

A vector field with cube Euclidean Lᵖ integrability and an Lᵖ fractional difference kernel of order s.

• toField : Vec d → Vec d
• euclideanMemLp : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (self.toField x)) p.exponent (normalizedCubeMeasure Q)
• euclideanMemWsp : MemCubeEuclideanWsp Q s p self.toField

@[instance_reducible]

instance HCPolySupport.CubeEuclideanWspField.instCoeFunForallVec {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} : CoeFun (CubeEuclideanWspField Q s p) fun (x : CubeEuclideanWspField Q s p) => Vec d → Vec d

Equations

• HCPolySupport.CubeEuclideanWspField.instCoeFunForallVec = { coe := fun (F : HCPolySupport.CubeEuclideanWspField Q s p) => F.toField }

theorem HCPolySupport.CubeEuclideanWspField.kernel_aestronglyMeasurable {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (F : CubeEuclideanWspField Q s p) : MeasureTheory.AEStronglyMeasurable (cubeEuclideanWspKernel s p F.toField) (Gagliardo.gagliardoCubeMeasure Q)

theorem HCPolySupport.CubeEuclideanWspField.eSeminorm_lt_top {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (F : CubeEuclideanWspField Q s p) : cubeEuclideanWspESeminorm Q s p F.toField < ⊤

noncomputable def HCPolySupport.cubeEuclideanWspScalePowerWeight {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) : ENNReal

The extended nonnegative scale weight given by the cube scale factor to the power -s p.

Equations

• HCPolySupport.cubeEuclideanWspScalePowerWeight Q s p = ENNReal.ofReal (HCPolySupport.cubeScaleFactor Q) ^ (-↑s * p.exponent.toReal)

theorem HCPolySupport.cubeEuclideanWspScalePowerWeight_lt_top {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) : cubeEuclideanWspScalePowerWeight Q s p < ⊤

noncomputable def HCPolySupport.cubeEuclideanWspFullENorm {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) : ENNReal

The extended full fractional norm: the pth root of the sum of the scale-weighted normalized Lᵖ norm to power p and the fractional seminorm to power p.

Equations

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

theorem HCPolySupport.CubeEuclideanWspField.normalizedEuclideanLpENorm_lt_top {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (F : CubeEuclideanWspField Q s p) : (cubeBoundedMeasurableDomain Q).normalizedEuclideanLpENorm p.exponent F.toField < ⊤

theorem HCPolySupport.CubeEuclideanWspField.fullENorm_lt_top {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (F : CubeEuclideanWspField Q s p) : cubeEuclideanWspFullENorm Q s p F.toField < ⊤