Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Measurable bases and measurable splittings of subspaces

Lax606786.MeasurableBases · concepts/Lax606786/MeasurableBases.lean · lax-606786

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Let XX be a separable Banach space with its Borel σ\sigma-algebra and k≥1k \ge 1.

    • There is a measurable map b:GkX→Xkb : \mathcal{G}_k X \to X^k such that b(V)b(V) spans VV for every VV. Composing with a measurable family E:Ω→GkXE : \Omega \to \mathcal{G}_k X gives a measurable choice of basis of E(ω)E(\omega).
    • There are measurable maps U:Gk+1X→GkXU : \mathcal{G}_{k+1} X \to \mathcal{G}_k X and u:Gk+1X→Xu : \mathcal{G}_{k+1} X \to X such that u(V)u(V) is a unit vector and V=U(V)+span⁡{u(V)}V = U(V) + \operatorname{span}\{u(V)\} for every VV.

    Each (k+1)(k+1)-dimensional subspace also contains a kk-dimensional subspace chosen measurably.

    Concept map
    2 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

    1 exists_measurable_basis proven

    2 exists_measurable_hyperplane proven

    3 exists_measurable_retract proven

    In the paper

    • page 5 of this submission's paper

    Lean source view on GitLab

    1import Lax606786.BanachGrassmannian
    2import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
    3
    4import Mathlib.Analysis.InnerProductSpace.PiL2
    5/-!
    6---
    7title: Measurable bases and measurable splittings of subspaces
    8type: theorem
    9---
    10Let XX be a separable Banach space with its Borel σ\sigma-algebra and k≥1k \ge 1.
    11
    12- There is a measurable map b:GkX→Xkb : \mathcal{G}_k X \to X^k such that b(V)b(V) spans VV for every
    13 VV. Composing with a measurable family E:Ω→GkXE : \Omega \to \mathcal{G}_k X gives a measurable
    14 choice of basis of E(ω)E(\omega).
    15- There are measurable maps U:Gk+1X→GkXU : \mathcal{G}_{k+1} X \to \mathcal{G}_k X and
    16 u:Gk+1X→Xu : \mathcal{G}_{k+1} X \to X such that u(V)u(V) is a unit vector and
    17 V=U(V)+span⁡{u(V)}V = U(V) + \operatorname{span}\{u(V)\} for every VV.
    18
    19Each (k+1)(k+1)-dimensional subspace also contains a kk-dimensional subspace chosen measurably.
    20-/
    21
    22namespace Lax606786.MeasurableBases
    23
    24open TopologicalSpace
    25open Lax606786.BanachGrassmannian
    26
    27variable {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    28
    29/-- A measurable spanning `k`-tuple for each `V ∈ 𝒢_k X`. -/
    30axiom exists_measurable_basis [SeparableSpace X] [CompleteSpace X] [MeasurableSpace X]
    31 [BorelSpace X] (k : ℕ) [NeZero k] :
    32 ∃ b : GrassmannianFin X k → Fin k → X,
    33 Measurable b ∧ ∀ V, (V.1 : Submodule ℝ X) = Submodule.span ℝ (Set.range (b V))
    34
    35/-- A measurable splitting of a `(k+1)`-dimensional subspace into a `k`-dimensional one and a
    36unit vector. -/
    37axiom exists_measurable_retract [SeparableSpace X] [CompleteSpace X] [MeasurableSpace X]
    38 [BorelSpace X] (k : ℕ) [NeZero k] :
    39 ∃ (U : GrassmannianFin X (k + 1) → GrassmannianFin X k) (u : GrassmannianFin X (k + 1) → X),
    40 Measurable U ∧ Measurable u ∧
    41 ∀ V, ‖u V‖ = 1 ∧ (U V).1 ⊔ Submodule.span ℝ {u V} = V.1
    42
    43/-- A measurable choice of a codimension-one subspace of each `(k+1)`-dimensional subspace. -/
    44axiom exists_measurable_hyperplane [SeparableSpace X] [CompleteSpace X] [MeasurableSpace X]
    45 [BorelSpace X] (k : ℕ) [NeZero k] :
    46 ∃ U : GrassmannianFin X (k + 1) → GrassmannianFin X k, Measurable U ∧
    47 ∀ V, (U V).1 < V.1
    48
    49end Lax606786.MeasurableBases
    50
    Show ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…