Documentation

LeanPool.ScottishBook155.CombinedEmbedding

Combining the relative and injectivity coordinates #

This module formalizes the abstract final assembly in the protected-extension proof. The still-missing relative Banach-envelope map is represented by an arbitrary first coordinate. Pairing it with the quotient Kuratowski coordinate in the max product preserves its metric estimates and supplies global injectivity once the first coordinate separates the collapsed subset.

source
noncomputable def ScottishBook155.combinedEmbedding {P : Type u} [MetricSpace P] {E : Type v} (relative : P → E) (S : Set P) (base x : P) :
E × ↥(lp (fun (x : CollapsedQuotient P S) => ℝ) ⊤)

Pair an arbitrary relative coordinate with the quotient Kuratowski coordinate used to recover injectivity.

Equations
Instances For
    source
    theorem ScottishBook155.combinedEmbedding_of_mem {P : Type u} [MetricSpace P] {E : Type v} {relative : P → E} {S : Set P} {base x : P} (hbase : base ∈ S) (hx : x ∈ S) :
    combinedEmbedding relative S base x = (relative x, 0)
    source
    theorem ScottishBook155.combinedEmbedding_eq_iff {P : Type u} [MetricSpace P] {E : Type v} {relative : P → E} {S : Set P} (hne : S.Nonempty) (hclosed : IsClosed S) (base x y : P) :
    combinedEmbedding relative S base x = combinedEmbedding relative S base y ↔ relative x = relative y ∧ (x = y ∨ x ∈ S ∧ y ∈ S)
    source
    theorem ScottishBook155.combinedEmbedding_injective {P : Type u} [MetricSpace P] {E : Type v} {relative : P → E} {S : Set P} (hne : S.Nonempty) (hclosed : IsClosed S) (hrelative : Set.InjOn relative S) (base : P) :
    Function.Injective (combinedEmbedding relative S base)

    The second coordinate separates all pairs except pairs in S; hence injectivity of the first coordinate on S implies global injectivity.

    source
    theorem ScottishBook155.combinedEmbedding_dist_le {P : Type u} [MetricSpace P] {E : Type v} [PseudoMetricSpace E] {relative : P → E} (hrelative : ∀ (x y : P), dist (relative x) (relative y) ≤ dist x y) (S : Set P) (base x y : P) :
    dist (combinedEmbedding relative S base x) (combinedEmbedding relative S base y) ≤ dist x y

    Pairing two nonexpansive coordinates in the max product is nonexpansive.

    source
    theorem ScottishBook155.combinedEmbedding_dist_eq {P : Type u} [MetricSpace P] {E : Type v} [PseudoMetricSpace E] {relative : P → E} {x y : P} (hrelative : dist (relative x) (relative y) = dist x y) (S : Set P) (base : P) :
    dist (combinedEmbedding relative S base x) (combinedEmbedding relative S base y) = dist x y

    If the first coordinate preserves a selected distance, then the combined max-product coordinate preserves it as well.