Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.ContinuousInterpolation.MeasurableRepresentative

Coarse-graining support: #

Support.Sobolev.Fractional.ContinuousInterpolation.MeasurableRepresentative

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

Measurable representatives of unit-cube Euclidean L² fields #

The public UnitCubeEuclideanL2Field carrier stores an a.e. L² witness, not a chosen measurable representative. This module obtains one internally from that witness without changing the carrier.

source
noncomputable def HCPolySupport.UnitCubeEuclideanL2Field.measurableRepresentative {d : ℕ} (F : UnitCubeEuclideanL2Field d) :
UnitCubeEuclideanL2Field d

The globally measurable vector representative selected from the stored Hilbert-valued Euclidean L² witness.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.UnitCubeEuclideanL2Field.measurable_measurableRepresentative {d : ℕ} (F : UnitCubeEuclideanL2Field d) :
    Measurable F.measurableRepresentative.toField

    The selected representative is globally measurable as a Vec d field.

    source
    theorem HCPolySupport.UnitCubeEuclideanL2Field.ae_eq_measurableRepresentative {d : ℕ} (F : UnitCubeEuclideanL2Field d) :
    F.toField =ᵐ[(unitCenteredCubeDomain d).normalizedVolume] F.measurableRepresentative.toField

    The chosen representative agrees with the original field almost everywhere for normalized unit-cube volume.

    source
    theorem HCPolySupport.UnitCubeEuclideanL2Field.measurableRepresentative_euclideanMemL2 {d : ℕ} (F : UnitCubeEuclideanL2Field d) :
    MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (F.measurableRepresentative.toField x)) 2 (unitCenteredCubeDomain d).normalizedVolume

    The representative retains the stored Euclidean L² witness.

    source
    theorem HCPolySupport.UnitCubeEuclideanL2Field.measurable_measurableRepresentative_coordinate {d : ℕ} (F : UnitCubeEuclideanL2Field d) (i : Fin d) :
    Measurable fun (x : Vec d) => F.measurableRepresentative.toField x i

    Every scalar coordinate of the selected representative is globally measurable.

    source
    theorem HCPolySupport.UnitCubeEuclideanL2Field.memLp_measurableRepresentative {d : ℕ} (F : UnitCubeEuclideanL2Field d) :
    MeasureTheory.MemLp F.measurableRepresentative.toField 2 (normalizedCubeMeasure (originCube d 0))

    The selected representative is an ambient-vector L² field for the canonical origin-cube normalization.

    source
    theorem HCPolySupport.UnitCubeEuclideanL2Field.memLp_measurableRepresentative_coordinate {d : ℕ} (F : UnitCubeEuclideanL2Field d) (i : Fin d) :
    MeasureTheory.MemLp (fun (x : Vec d) => F.measurableRepresentative.toField x i) 2 (normalizedCubeMeasure (originCube d 0))

    Every scalar coordinate of the selected representative is in L² for the canonical origin-cube normalization.

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

    Replacing a field by its chosen measurable representative preserves the continuous interpolation seminorm.

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

    Replacing a field by its chosen measurable representative preserves the exact Euclidean fractional energy.

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

    Replacing a field by its chosen measurable representative preserves the exact Euclidean fractional seminorm.