Documentation

LeanModulus.Common.ToReal

The ℝ≥0 → ℝ bridge for densities #

The bridge from Density E := E → ℝ≥0 (see LeanModulus.Common.FamilyOfObjects) into E → ℝ, via the coercion Density.toReal. Real-analysis tools (compactness, Krein-Milman) aren't available directly over ℝ≥0, so this file collects the algebra of toReal (additivity, scalar multiples), the fact that it's a closed embedding, and the consequences for Γ.Adm's image (convexity, closedness, nonemptiness) needed to move the duality argument into a locally convex TVS over ℝ.

Everything here genuinely needs toReal; facts about Density E/Γ.Adm that don't mention it (e.g. their intrinsic ℝ≥0-side topology) belong in LeanModulus.Common.FamilyOfObjects instead.

source
def Density.toReal {E : Type u_1} (ρ : Density E) :
E → ℝ

The coercion of a density E → ℝ≥0 into a real-valued function E → ℝ.

Equations
Instances For
    source
    theorem Density.toReal_nonneg {E : Type u_1} (ρ : Density E) :
    0 ≤ ρ.toReal

    The coercion of a density to a real-valued function is nonnegative.

    source
    theorem Density.toReal_add {E : Type u_1} (ρ₁ ρ₂ : Density E) :
    (ρ₁ + ρ₂).toReal = ρ₁.toReal + ρ₂.toReal

    The length with respect to the sum of two densities is the sum of the lengths.

    source
    theorem Density.toReal_smul {E : Type u_1} (c : NNReal) (ρ : Density E) :
    (c • ρ).toReal = ↑c • ρ.toReal

    The length with respect to a scalar multiple of a density is the scalar multiple of the length.

    source
    theorem Density.isClosedEmbedding_toReal {E : Type u_1} :
    Topology.IsClosedEmbedding toReal

    The coercion of a density E → ℝ≥0 into a real-valued function E → ℝ is a closed embedding.

    source
    theorem Density.toReal_injective {E : Type u_1} :
    Function.Injective toReal

    The coercion of a density E → ℝ≥0 into a real-valued function E → ℝ is injective.

    source
    theorem Density.toReal_image_openSegment {E : Type u_1} (ρ₁ ρ₂ : Density E) :
    toReal '' openSegment NNReal ρ₁ ρ₂ = openSegment ℝ ρ₁.toReal ρ₂.toReal

    The image of an open segment under toReal is an open segment.

    source
    theorem FamilyOfObjects.convex_toReal_image_adm {E : Type u_1} [Finite E] (Γ : FamilyOfObjects E) :
    Convex ℝ (Density.toReal '' Γ.Adm)

    The image of Γ.Adm under toReal is convex.

    source
    theorem FamilyOfObjects.isClosed_toReal_image_adm {E : Type u_1} [Finite E] (Γ : FamilyOfObjects E) :
    IsClosed (Density.toReal '' Γ.Adm)

    The image of Γ.Adm under toReal is closed.

    source
    theorem FamilyOfObjects.nonempty_toReal_image_adm {E : Type u_1} (Γ : FamilyOfObjects E) (h : Γ.Adm.Nonempty) :
    (Density.toReal '' Γ.Adm).Nonempty

    The image of Γ.Adm under toReal is nonempty whenever Γ.Adm is nonempty.

    source
    theorem FamilyOfObjects.toReal_mem_extremePoints_of_mem_fulkersonDual {E : Type u_1} (Γ : FamilyOfObjects E) (ρ : Density E) (hρ : ρ ∈ Γ.FulkersonDual) :
    ρ.toReal ∈ Set.extremePoints ℝ (Density.toReal '' Γ.Adm)

    A point in Γ.FulkersonDual is an extreme point of the image of Γ.Adm under toReal.

    source
    theorem FamilyOfObjects.mem_fulkersonDual_of_toReal_mem_extremePoints {E : Type u_1} (Γ : FamilyOfObjects E) (ρ : Density E) (hρ : ρ.toReal ∈ Set.extremePoints ℝ (Density.toReal '' Γ.Adm)) :
    ρ ∈ Γ.FulkersonDual

    An extreme point of the image of Γ.Adm under toReal belongs to Γ.FulkersonDual.

    source
    theorem FamilyOfObjects.toReal_image_fulkersonDual {E : Type u_1} (Γ : FamilyOfObjects E) :
    Density.toReal '' Γ.FulkersonDual = Set.extremePoints ℝ (Density.toReal '' Γ.Adm)

    The image of Γ.FulkersonDual under toReal is the set of extreme points of the image of Γ.Adm under toReal.