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

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

Euclidean L² fields on the unit centered cube

This common source-facing carrier is the Euclidean vector L² input used by the Chapter 1 analytic kernels on the unit centered cube.

noncomputable def HCPolySupport.unitCenteredCubeDomain (d : ℕ) : BoundedMeasurableDomain d

The bounded measurable realization of the unit centered cube.

Equations

• HCPolySupport.unitCenteredCubeDomain d = HCPolySupport.cubeBoundedMeasurableDomain (HCPolySupport.originCube d 0)

@[reducible, inline]

abbrev HCPolySupport.FractionalOrder : Set ℝ

The common fractional-order carrier 0 < s < 1.

Equations

• HCPolySupport.FractionalOrder = Set.Ioo 0 1

theorem HCPolySupport.FractionalOrder.pos (s : ↑FractionalOrder) : 0 < ↑s

theorem HCPolySupport.FractionalOrder.lt_one (s : ↑FractionalOrder) : ↑s < 1

structure HCPolySupport.UnitCubeEuclideanL2Field (d : ℕ) : Type

A Euclidean L² vector field on the unit centered cube. The witness uses the Euclidean Hilbert realization, so it supplies the explicit euclideanNorm L² fact without a finite-real fallback.

• toField : Vec d → Vec d

  The represented vector field.

• euclideanMemL2 : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (self.toField x)) 2 (unitCenteredCubeDomain d).normalizedVolume

@[instance_reducible]

instance HCPolySupport.UnitCubeEuclideanL2Field.instCoeFunForallVec {d : ℕ} : CoeFun (UnitCubeEuclideanL2Field d) fun (x : UnitCubeEuclideanL2Field d) => Vec d → Vec d

Equations

• HCPolySupport.UnitCubeEuclideanL2Field.instCoeFunForallVec = { coe := fun (F : HCPolySupport.UnitCubeEuclideanL2Field d) => F.toField }

theorem HCPolySupport.UnitCubeEuclideanL2Field.euclideanMagnitudeMemL2 {d : ℕ} (F : UnitCubeEuclideanL2Field d) : MeasureTheory.MemLp (fun (x : Vec d) => euclideanNorm (F.toField x)) 2 (unitCenteredCubeDomain d).normalizedVolume

The explicit Euclidean-magnitude form of the stored L² fact.