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

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

Euclidean L² fields on centered triadic cubes

This module transports the exact Euclidean L² carrier between the centered triadic cube at scale m and the centered unit cube. The transport uses the literal dilation x ↦ (3 ^ m) • x; normalized volume is therefore preserved exactly.

Main definitions

• centeredCubeDomain: the bounded measurable realization of originCube d m.
• CenteredCubeEuclideanL2Field: Euclidean L² vector fields on that domain.
• CenteredCubeEuclideanL2Field.pullbackToUnit: pullback by the cube dilation.

Main results

• centeredCubeDilationMeasurePreserving: normalized-volume preservation.
• normalizedEuclideanLpENorm_pullbackToUnit: exact normalized norm invariance.

noncomputable def HCPolySupport.centeredCubeDomain (d : ℕ) (m : ℤ) : BoundedMeasurableDomain d

The bounded measurable realization of the centered triadic cube at scale m.

Equations

• HCPolySupport.centeredCubeDomain d m = HCPolySupport.cubeBoundedMeasurableDomain (HCPolySupport.originCube d m)

noncomputable def HCPolySupport.centeredCubeScale (m : ℤ) : ℝ

The positive dilation factor carrying the centered unit cube to scale m.

Equations

• HCPolySupport.centeredCubeScale m = 3 ^ m

@[simp]

theorem HCPolySupport.centeredCubeScale_zero : centeredCubeScale 0 = 1

theorem HCPolySupport.centeredCubeScale_pos (m : ℤ) : 0 < centeredCubeScale m

theorem HCPolySupport.centeredCubeScale_ne_zero (m : ℤ) : centeredCubeScale m ≠ 0

noncomputable def HCPolySupport.centeredCubeDilation {d : ℕ} (m : ℤ) : Vec d → Vec d

Dilation from the centered unit cube to the centered cube at scale m.

Equations

• HCPolySupport.centeredCubeDilation m x = HCPolySupport.centeredCubeScale m • x

theorem HCPolySupport.measurable_centeredCubeDilation {d : ℕ} (m : ℤ) : Measurable (centeredCubeDilation m)

theorem HCPolySupport.map_centeredCubeDilation_restrictedVolume {d : ℕ} (m : ℤ) : MeasureTheory.Measure.map (centeredCubeDilation m) (centeredCubeDomain d 0).restrictedVolume = ENNReal.ofReal (centeredCubeScale m ^ d)⁻¹ • (centeredCubeDomain d m).restrictedVolume

Restricted volume gains the inverse Jacobian under centered-cube dilation.

theorem HCPolySupport.map_centeredCubeDilation_normalizedVolume {d : ℕ} (m : ℤ) : MeasureTheory.Measure.map (centeredCubeDilation m) (centeredCubeDomain d 0).normalizedVolume = (centeredCubeDomain d m).normalizedVolume

Normalized volume is exactly preserved by centered-cube dilation.

theorem HCPolySupport.centeredCubeDilationMeasurePreserving {d : ℕ} (m : ℤ) : MeasureTheory.MeasurePreserving (centeredCubeDilation m) (centeredCubeDomain d 0).normalizedVolume (centeredCubeDomain d m).normalizedVolume

Centered-cube dilation as a normalized-volume-preserving map.

structure HCPolySupport.CenteredCubeEuclideanL2Field (d : ℕ) (m : ℤ) : Type

A Euclidean L² vector field on the centered cube at scale m.

• toField : Vec d → Vec d

  The represented vector field.

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

@[instance_reducible]

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

Equations

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

theorem HCPolySupport.CenteredCubeEuclideanL2Field.euclideanMagnitudeMemL2 {d : ℕ} {m : ℤ} (F : CenteredCubeEuclideanL2Field d m) : MeasureTheory.MemLp (fun (x : Vec d) => euclideanNorm (F.toField x)) 2 (centeredCubeDomain d m).normalizedVolume

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

noncomputable def HCPolySupport.CenteredCubeEuclideanL2Field.pullbackToUnit {d : ℕ} {m : ℤ} (F : CenteredCubeEuclideanL2Field d m) : UnitCubeEuclideanL2Field d

Pull a physical centered-cube field back to the centered unit cube.

Equations

• F.pullbackToUnit = { toField := fun (x : HCPolySupport.Vec d) => F.toField (HCPolySupport.centeredCubeDilation m x), euclideanMemL2 := ⋯ }

@[simp]

theorem HCPolySupport.CenteredCubeEuclideanL2Field.pullbackToUnit_apply {d : ℕ} {m : ℤ} (F : CenteredCubeEuclideanL2Field d m) (x : Vec d) : F.pullbackToUnit.toField x = F.toField (centeredCubeScale m • x)

noncomputable def HCPolySupport.CenteredCubeEuclideanL2Field.measurableRepresentative {d : ℕ} {m : ℤ} (F : CenteredCubeEuclideanL2Field d m) : CenteredCubeEuclideanL2Field d m

A globally measurable representative selected from the stored Euclidean L² witness on the centered cube.

Equations

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

theorem HCPolySupport.CenteredCubeEuclideanL2Field.measurable_measurableRepresentative {d : ℕ} {m : ℤ} (F : CenteredCubeEuclideanL2Field d m) : Measurable F.measurableRepresentative.toField

The selected centered-cube representative is globally measurable.

theorem HCPolySupport.CenteredCubeEuclideanL2Field.ae_eq_measurableRepresentative {d : ℕ} {m : ℤ} (F : CenteredCubeEuclideanL2Field d m) : F.toField =ᵐ[(centeredCubeDomain d m).normalizedVolume] F.measurableRepresentative.toField

The selected representative agrees with the original field almost everywhere for normalized centered-cube volume.

theorem HCPolySupport.CenteredCubeEuclideanL2Field.normalizedEuclideanLpENorm_pullbackToUnit {d : ℕ} {m : ℤ} (F : CenteredCubeEuclideanL2Field d m) : (unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 F.pullbackToUnit.toField = (centeredCubeDomain d m).normalizedEuclideanLpENorm 2 F.toField

Pullback preserves the exact normalized Euclidean extended L² norm.

theorem HCPolySupport.CenteredCubeEuclideanL2Field.normalizedEuclideanLpNorm_pullbackToUnit {d : ℕ} {m : ℤ} (F : CenteredCubeEuclideanL2Field d m) : (unitCenteredCubeDomain d).normalizedEuclideanLpNorm 2 F.pullbackToUnit.toField ⋯ = (centeredCubeDomain d m).normalizedEuclideanLpNorm 2 F.toField ⋯

Pullback preserves the proof-carrying normalized Euclidean real L² norm.