Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.ContinuousInterpolation.AllDimensionalComposition

Coarse-graining support: #

Support.Sobolev.Fractional.ContinuousInterpolation.AllDimensionalComposition

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

All-dimensional composition of sampled continuous K and Euclidean energies #

This module removes the positive-dimension and measurability hypotheses from the energy comparisons. Dimension zero is closed exactly, while positive dimensions use the chosen measurable representative.

source
theorem HCPolySupport.triadicContinuousKSampleTerm_congr_ae {d : ℕ} (s : ↑FractionalOrder) {F H : UnitCubeEuclideanL2Field d} (hFH : F.toField =ᵐ[(unitCenteredCubeDomain d).normalizedVolume] H.toField) (j : ℕ) :
triadicContinuousKSampleTerm s F j = triadicContinuousKSampleTerm s H j

A normalized-volume a.e. replacement preserves each weighted triadic continuous K sample.

source
theorem HCPolySupport.triadicContinuousKSampleEnergy_congr_ae {d : ℕ} (s : ↑FractionalOrder) {F H : UnitCubeEuclideanL2Field d} (hFH : F.toField =ᵐ[(unitCenteredCubeDomain d).normalizedVolume] H.toField) :
triadicContinuousKSampleEnergy s F = triadicContinuousKSampleEnergy s H

A normalized-volume a.e. replacement preserves the full triadic sampled continuous K energy.

source
theorem HCPolySupport.triadicContinuousKShiftedSampleEnergy_congr_ae {d : ℕ} (s : ↑FractionalOrder) {F H : UnitCubeEuclideanL2Field d} (hFH : F.toField =ᵐ[(unitCenteredCubeDomain d).normalizedVolume] H.toField) :
triadicContinuousKShiftedSampleEnergy s F = triadicContinuousKShiftedSampleEnergy s H

A normalized-volume a.e. replacement preserves the endpoint-excluded triadic sampled continuous K energy.

source
theorem HCPolySupport.UnitCubeEuclideanL2Field.triadicContinuousKSampleEnergy_eq_measurableRepresentative {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) :
triadicContinuousKSampleEnergy s F = triadicContinuousKSampleEnergy s F.measurableRepresentative

The selected measurable representative preserves the full triadic sampled continuous K energy.

source
noncomputable def HCPolySupport.allDimensionalSampleToHsConstant (s : ↑FractionalOrder) (d : ℕ) :
ENNReal

The all-dimensional finite constant for the sampled-energy to Euclidean-energy direction.

Equations
Instances For
    source
    noncomputable def HCPolySupport.allDimensionalHsToSampleConstant (d : ℕ) :
    ENNReal

    The all-dimensional finite constant for the Euclidean-energy to sampled-energy direction.

    Equations
    Instances For
      source
      theorem HCPolySupport.allDimensionalSampleToHsConstant_lt_top (s : ↑FractionalOrder) (d : ℕ) :
      allDimensionalSampleToHsConstant s d < ⊤
      source
      theorem HCPolySupport.allDimensionalHsToSampleConstant_lt_top (d : ℕ) :
      allDimensionalHsToSampleConstant d < ⊤
      source
      theorem HCPolySupport.euclideanHsEnergy_le_mul_triadicContinuousKSampleEnergy_all_dim {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) :
      euclideanHsEnergy s F ≤ allDimensionalHsToSampleConstant d * triadicContinuousKSampleEnergy s F

      In every dimension, the sampled continuous K energy controls the exact Euclidean H^s energy.

      source
      theorem HCPolySupport.triadicContinuousKSampleEnergy_le_mul_euclideanHsEnergy_all_dim {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) :
      triadicContinuousKSampleEnergy s F ≤ allDimensionalSampleToHsConstant s d * euclideanHsEnergy s F

      In every dimension, the exact Euclidean H^s energy controls the sampled continuous K energy.

      source
      theorem HCPolySupport.euclideanHsEnergy_lt_top_iff_triadicContinuousKSampleEnergy_lt_top {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) :
      euclideanHsEnergy s F < ⊤ ↔ triadicContinuousKSampleEnergy s F < ⊤

      The exact Euclidean and sampled continuous K energies are finite under the same condition in every dimension.