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

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

Exact Euclidean fractional H^s on centered triadic cubes

This module defines the literal physical-cube Gagliardo energy with normalized volume in its first variable and unnormalized restricted volume in its second. It then transports that energy to the centered unit cube under x ↦ (3 ^ m) • x.

Main definitions

• centeredCubeEuclideanHsProductMeasure: the physical product measure.
• centeredCubeEuclideanHsEnergy: the literal physical Euclidean energy.
• centeredCubeEuclideanHsESeminorm: its extended square root.
• MemCenteredCubeEuclideanHs: measurable finite-energy membership.

Main results

• centeredCubeEuclideanHsEnergy_eq_scale_mul_pullbackToUnit: exact (3 ^ m) ^ (-2s) energy scaling.
• centeredCubeEuclideanHsESeminorm_eq_scale_mul_pullbackToUnit: exact (3 ^ m) ^ (-s) seminorm scaling.
• memCenteredCubeEuclideanHs_iff_pullbackToUnit: exact membership transport.

noncomputable def HCPolySupport.centeredCubeEuclideanHsProductMeasure (d : ℕ) (m : ℤ) : MeasureTheory.Measure (Vec d × Vec d)

The source measure fint_{□_m} dx ∫_{□_m} dy: normalized volume in the first variable and unnormalized restricted volume in the second.

Equations

• HCPolySupport.centeredCubeEuclideanHsProductMeasure d m = (HCPolySupport.centeredCubeDomain d m).normalizedVolume.prod (HCPolySupport.centeredCubeDomain d m).restrictedVolume

theorem HCPolySupport.centeredCubeEuclideanHsProductMeasure_eq_gagliardoCubeMeasure (d : ℕ) (m : ℤ) : centeredCubeEuclideanHsProductMeasure d m = Gagliardo.gagliardoCubeMeasure (originCube d m)

The physical product measure is exactly the established Gagliardo cube measure, with no additional normalization convention.

noncomputable def HCPolySupport.centeredCubeEuclideanHsIntegrand {d : ℕ} {m : ℤ} (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) : Vec d × Vec d → ENNReal

The literal physical integrand |F(x)-F(y)|² / |x-y|^(d + 2s) on the centered cube at scale m.

Equations

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

noncomputable def HCPolySupport.centeredCubeEuclideanHsEnergy {d : ℕ} {m : ℤ} (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) : ENNReal

The squared physical Euclidean fractional quantity.

Equations

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

noncomputable def HCPolySupport.centeredCubeEuclideanHsESeminorm {d : ℕ} {m : ℤ} (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) : ENNReal

The exact extended Euclidean fractional seminorm on the centered cube.

Equations

• HCPolySupport.centeredCubeEuclideanHsESeminorm s F = HCPolySupport.centeredCubeEuclideanHsEnergy s F ^ 2⁻¹

structure HCPolySupport.MemCenteredCubeEuclideanHs {d : ℕ} {m : ℤ} (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) : Prop

Membership in the literal physical centered-cube Euclidean H^s carrier.

• integrand_aemeasurable : AEMeasurable (centeredCubeEuclideanHsIntegrand s F) (centeredCubeEuclideanHsProductMeasure d m)
• energy_lt_top : centeredCubeEuclideanHsEnergy s F < ⊤

theorem HCPolySupport.centeredCubeEuclideanHsEnergy_eq_lintegral {d : ℕ} {m : ℤ} (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) : centeredCubeEuclideanHsEnergy s F = ∫⁻ (z : Vec d × Vec d), ENNReal.ofReal (‖HilbertVec.ofVec (F.toField z.1 - F.toField z.2)‖ ^ 2 / (euclideanDist z.1 z.2).rpow (↑d + 2 * ↑s)) ∂centeredCubeEuclideanHsProductMeasure d m

Formula accessor for the physical squared energy.

theorem HCPolySupport.centeredCubeEuclideanHsESeminorm_eq_lintegral {d : ℕ} {m : ℤ} (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) : centeredCubeEuclideanHsESeminorm s F = (∫⁻ (z : Vec d × Vec d), ENNReal.ofReal (‖HilbertVec.ofVec (F.toField z.1 - F.toField z.2)‖ ^ 2 / (euclideanDist z.1 z.2).rpow (↑d + 2 * ↑s)) ∂centeredCubeEuclideanHsProductMeasure d m) ^ 2⁻¹

Formula accessor for the physical extended seminorm.

theorem HCPolySupport.centeredCubeEuclideanHsIntegrand_congr_ae {d : ℕ} {m : ℤ} {s : ↑FractionalOrder} {F G : CenteredCubeEuclideanL2Field d m} (hFG : F.toField =ᵐ[(centeredCubeDomain d m).normalizedVolume] G.toField) : centeredCubeEuclideanHsIntegrand s F =ᵐ[centeredCubeEuclideanHsProductMeasure d m] centeredCubeEuclideanHsIntegrand s G

The physical integrand is invariant under normalized-volume a.e. replacement of the field.

theorem HCPolySupport.centeredCubeEuclideanHsEnergy_congr_ae {d : ℕ} {m : ℤ} {s : ↑FractionalOrder} {F G : CenteredCubeEuclideanL2Field d m} (hFG : F.toField =ᵐ[(centeredCubeDomain d m).normalizedVolume] G.toField) : centeredCubeEuclideanHsEnergy s F = centeredCubeEuclideanHsEnergy s G

The physical squared energy is invariant under normalized-volume a.e. replacement of the field.

theorem HCPolySupport.centeredCubeEuclideanHsESeminorm_congr_ae {d : ℕ} {m : ℤ} {s : ↑FractionalOrder} {F G : CenteredCubeEuclideanL2Field d m} (hFG : F.toField =ᵐ[(centeredCubeDomain d m).normalizedVolume] G.toField) : centeredCubeEuclideanHsESeminorm s F = centeredCubeEuclideanHsESeminorm s G

The physical extended seminorm is invariant under normalized-volume a.e. replacement of the field.

theorem HCPolySupport.aemeasurable_centeredCubeEuclideanHsIntegrand {d : ℕ} {m : ℤ} (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) : AEMeasurable (centeredCubeEuclideanHsIntegrand s F) (centeredCubeEuclideanHsProductMeasure d m)

The physical Euclidean integrand is a.e.-measurable for every stored centered-cube L² field.

theorem HCPolySupport.memCenteredCubeEuclideanHs_iff_energy_lt_top {d : ℕ} {m : ℤ} (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) : MemCenteredCubeEuclideanHs s F ↔ centeredCubeEuclideanHsEnergy s F < ⊤

Physical centered-cube membership is exactly finite physical energy.

noncomputable def HCPolySupport.centeredCubeDilationMeasurableEquiv {d : ℕ} (m : ℤ) : Vec d ≃ᵐ Vec d

The measurable equivalence implementing centered-cube dilation.

Equations

• HCPolySupport.centeredCubeDilationMeasurableEquiv m = (Homeomorph.smulOfNeZero (HCPolySupport.centeredCubeScale m) ⋯).toMeasurableEquiv

@[simp]

theorem HCPolySupport.centeredCubeDilationMeasurableEquiv_apply {d : ℕ} (m : ℤ) (x : Vec d) : (centeredCubeDilationMeasurableEquiv m) x = centeredCubeDilation m x

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

Dilation applied in both variables of the physical product measure.

Equations

• HCPolySupport.centeredCubePairDilation m = Prod.map (HCPolySupport.centeredCubeDilation m) (HCPolySupport.centeredCubeDilation m)

theorem HCPolySupport.map_centeredCubePairDilation_productMeasure {d : ℕ} (m : ℤ) : MeasureTheory.Measure.map (centeredCubePairDilation m) (centeredCubeEuclideanHsProductMeasure d 0) = ENNReal.ofReal (centeredCubeScale m ^ d)⁻¹ • centeredCubeEuclideanHsProductMeasure d m

The product measure gains exactly the inverse Jacobian from its unnormalized second variable under dilation.

theorem HCPolySupport.centeredCubeEuclideanHsProductMeasure_eq_smul_map {d : ℕ} (m : ℤ) : centeredCubeEuclideanHsProductMeasure d m = ENNReal.ofReal (centeredCubeScale m ^ d) • MeasureTheory.Measure.map (centeredCubePairDilation m) (centeredCubeEuclideanHsProductMeasure d 0)

The physical product measure is the Jacobian multiple of the pushforward of the unit product measure.

theorem HCPolySupport.centeredCubeEuclideanHsEnergy_eq_scale_mul_pullbackToUnit {d : ℕ} {m : ℤ} (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) : centeredCubeEuclideanHsEnergy s F = ENNReal.ofReal (centeredCubeScale m) ^ (-2 * ↑s) * euclideanHsEnergy s F.pullbackToUnit

Exact physical energy scaling under pullback to the centered unit cube.

theorem HCPolySupport.centeredCubeEuclideanHsESeminorm_eq_scale_mul_pullbackToUnit {d : ℕ} {m : ℤ} (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) : centeredCubeEuclideanHsESeminorm s F = ENNReal.ofReal (centeredCubeScale m) ^ (-↑s) * euclideanHsESeminorm s F.pullbackToUnit

Exact physical seminorm scaling under pullback to the centered unit cube.

theorem HCPolySupport.memCenteredCubeEuclideanHs_iff_pullbackToUnit {d : ℕ} {m : ℤ} (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) : MemCenteredCubeEuclideanHs s F ↔ MemEuclideanHs s F.pullbackToUnit

Physical centered-cube fractional membership is exactly membership of the unit pullback.