BoundaryDiagonalMeasurable.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Measurability of diagonal least-norm vectors

Finite rational convex expressions form a countable dense subset of each closed convex hull. Choosing the first expression within a specified squared-norm tolerance gives measurable approximants; the parallelogram identity forces their convergence to the unique least vector.

inductive OAI.KadisonKastler.RationalConvexExpr line 28
Source documentation
A countable syntax for rational convex combinations. Clamping the rational parameter avoids proof fields in the syntax.
```
inductive RationalConvexExpr (ι : Type*) where
…
```
def OAI.KadisonKastler.convexParameter line 33
theorem OAI.KadisonKastler.convexParameter_nonneg line 35
theorem OAI.KadisonKastler.convexParameter_le_one line 36
theorem OAI.KadisonKastler.convexParameter_eq line 38

def OAI.KadisonKastler.RationalConvexExpr.eval line 46

Source documentation

Evaluation of the rational convex syntax.

def eval (v : ι → E) : RationalConvexExpr ι → E
  | leaf i => v i
  | blend q a b => convexParameter (q : ℝ) • eval v a +
      (1 - convexParameter (q : ℝ)) • eval v b

/-- Every expression belongs to the ordinary convex hull of its leaves. -/

Mentions: OAI.KadisonKastler.RationalConvexExpr, OAI.KadisonKastler.convexParameter

theorem OAI.KadisonKastler.RationalConvexExpr.eval_mem_convexHull line 52
Source documentation
Every expression belongs to the ordinary convex hull of its leaves.
```
theorem eval_mem_convexHull (v : ι → E) (a : RationalConvexExpr ι) :
    eval v a ∈ convexHull ℝ (Set.range v) := by
…
```
Mentions: OAI.KadisonKastler.RationalConvexExpr, OAI.KadisonKastler.RationalConvexExpr.eval
theorem OAI.KadisonKastler.RationalConvexExpr.convex_closure_range_eval line 62
Source documentation
The closure of rational combinations is closed under all real convex combinations, by density of the rational parameters.
```
theorem convex_closure_range_eval (v : ι → E) :
    Convex ℝ (closure (Set.range (eval v))) := by
…
```
Mentions: OAI.KadisonKastler.RationalConvexExpr.eval
theorem OAI.KadisonKastler.RationalConvexExpr.closure_range_eval line 82
Source documentation
Rational convex expressions are dense in the real convex hull.
```
theorem closure_range_eval (v : ι → E) :
    closure (Set.range (eval v)) = closure (convexHull ℝ (Set.range v)) := by
…
```
Mentions: OAI.KadisonKastler.RationalConvexExpr.eval
theorem OAI.KadisonKastler.RationalConvexExpr.stronglyMeasurable_eval line 92
Source documentation
Evaluation preserves strong measurability of a family of leaves.
```
theorem stronglyMeasurable_eval {P : Type*} [MeasurableSpace P]
    (v : ι → P → E) (hv : ∀ i, StronglyMeasurable (v i)) (a : RationalConvexExpr ι) :
    StronglyMeasurable (fun p => eval (fun i => v i p) a) := by
…
```
Mentions: OAI.KadisonKastler.RationalConvexExpr, OAI.KadisonKastler.RationalConvexExpr.eval

theorem OAI.KadisonKastler.RationalConvexExpr.aestronglyMeasurable_eval line 100

Source documentation

Evaluation preserves almost-everywhere strong measurability.

theorem aestronglyMeasurable_eval {P : Type*} [MeasurableSpace P] {μ : Measure P}
    (v : ι → P → E) (hv : ∀ i, AEStronglyMeasurable (v i) μ) (a : RationalConvexExpr ι) :
    AEStronglyMeasurable (fun p => eval (fun i => v i p) a) μ := by
…

Mentions: OAI.KadisonKastler.RationalConvexExpr, OAI.KadisonKastler.RationalConvexExpr.eval

theorem OAI.KadisonKastler.norm_sub_sq_le_twice_gap line 114

Source documentation

A squared-norm tolerance controls distance to a least vector.

theorem norm_sub_sq_le_twice_gap {K : Set E} (hK : Convex ℝ K)
    {c z : E} (hc : c ∈ K) (hz : z ∈ K) (hmin : ∀ y ∈ K, ‖c‖ ≤ ‖y‖) :
    ‖z - c‖ ^ 2 ≤ 2 * (‖z‖ ^ 2 - ‖c‖ ^ 2) := by
…

theorem OAI.KadisonKastler.iInf_norm_sq_eq_least line 128

Source documentation

The infimum over a dense countable family is the least squared norm.

theorem iInf_norm_sq_eq_least (z : ℕ → E) (c : E)
    (hc : c ∈ closure (Set.range z))
    (hmin : ∀ y ∈ closure (Set.range z), ‖c‖ ≤ ‖y‖) :
    (⨅ n, ‖z n‖ ^ 2) = ‖c‖ ^ 2 := by
…

theorem OAI.KadisonKastler.stronglyMeasurable_countable_least line 148

Source documentation

The first countable approximant with almost least squared norm is a measurable function; its limit is the least vector.

theorem stronglyMeasurable_countable_least (z : ℕ → P → E)
    (hz : ∀ n, StronglyMeasurable (z n)) (c : P → E)
    (hc : ∀ p, c p ∈ closure (Set.range (fun n => z n p)))
    (hconv : ∀ p, Convex ℝ (closure (Set.range (fun n => z n p))))
    (hmin : ∀ p y, y ∈ closure (Set.range (fun n => z n p)) → ‖c p‖ ≤ ‖y‖) :
    StronglyMeasurable c := by
…

theorem OAI.KadisonKastler.stronglyMeasurable_convex_least line 194

Source documentation

The least vector of the closed convex hull of countably many strongly measurable Hilbert-valued fields is strongly measurable.

theorem stronglyMeasurable_convex_least {ι : Type*} [Countable ι] [Nonempty ι]
    (v : ι → P → E) (hv : ∀ i, StronglyMeasurable (v i)) (c : P → E)
    (hc : ∀ p, c p ∈ closure (convexHull ℝ (Set.range (fun i => v i p))))
    (hmin : ∀ p y, y ∈ closure (convexHull ℝ (Set.range (fun i => v i p))) →
      ‖c p‖ ≤ ‖y‖) : StronglyMeasurable c := by
…

theorem OAI.KadisonKastler.aestronglyMeasurable_convex_least line 223

Source documentation

Almost-everywhere measurable generators suffice: choose measurable versions of the leaves, apply the explicit countable approximation, and use uniqueness on the common conull set.

theorem aestronglyMeasurable_convex_least [CompleteSpace E]
    {ι : Type*} [Countable ι] [Nonempty ι] {μ : Measure P}
    (v : ι → P → E) (hv : ∀ i, AEStronglyMeasurable (v i) μ) (c : P → E)
    (hc : ∀ p, c p ∈ closure (convexHull ℝ (Set.range (fun i => v i p))))
    (hmin : ∀ p y, y ∈ closure (convexHull ℝ (Set.range (fun i => v i p))) →
      ‖c p‖ ≤ ‖y‖) : AEStronglyMeasurable c μ := by
…

theorem OAI.KadisonKastler.aestronglyMeasurable_diagonal_least line 251

Source documentation

Measurability of the actual diagonal least operator in its supplied separable trace Hilbert realization.

theorem aestronglyMeasurable_diagonal_least
    {H E P ι : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [SeparableSpace E]
    [MeasurableSpace E] [BorelSpace E] [MeasurableSpace P] [Countable ι] [Nonempty ι]
    {M : VonNeumannAlgebra H} (J : Algebra M →ₗ[ℂ] E) {μ : Measure P}
    (v : ι → P → Algebra M)
    (hv : ∀ i, AEStronglyMeasurable (fun p => J (v i p)) μ)
    (c : P → Algebra M)
    (hc : ∀ p, J (c p) ∈ diagonalTraceHull J (Set.range (fun i => v i p)))
    (hmin : ∀ p y, y ∈ diagonalTraceHull J (Set.range (fun i => v i p)) →
      ‖J (c p)‖ ≤ ‖y‖) : AEStronglyMeasurable (fun p => J (c p)) μ := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.diagonalTraceHull

theorem OAI.KadisonKastler.exists_measurable_diagonal_least_field line 289

Source documentation

The actual diagonal least field has a measurable trace-Hilbert realization, full least-vector properties, and exact covariance.

theorem exists_measurable_diagonal_least_field
    {G D : Type*} [Group G] [Countable G] [MeasurableSpace D] {μ : Measure (D × D)}
    (shift : G → D → D) (W : G → D → unitary (Algebra M))
    (hW : ∀ g t x, (W (g * t) x : Algebra M) =
      (W g x : Algebra M) * (W t (shift g x) : Algebra M))
    (hWmeas : ∀ t, AEStronglyMeasurable
      (fun p : D × D => J ((W t p.1 : Algebra M) * star (W t p.2 : Algebra M))) μ)
    {r : ℝ} (hr : 0 ≤ r)
    (hnear : ∀ t x y, ‖(W t x : Algebra M) * star (W t y : Algebra M) - 1‖ ≤ r) :
    ∃ c : D → D → Algebra M,
      AEStronglyMeasurable (fun p : D × D => J (c p.1 p.2)) μ ∧
      (∀ x y, J (c x y) ∈ diagonalTraceHull J (diagonalGenerators W x y) ∧
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.diagonalTraceHull, OAI.KadisonKastler.diagonalGenerators

theorem OAI.KadisonKastler.exists_measurable_diagonal_polar_data line 315

Source documentation

Measurable least-field data together with its exact unitary polar factor. The trace-Hilbert measurability assertion concerns the least field; operator measurability of its polar factor is a separate transfer.

theorem exists_measurable_diagonal_polar_data
    {G D : Type*} [Group G] [Countable G] [MeasurableSpace D] {μ : Measure (D × D)}
    (shift : G → D → D) (W : G → D → unitary (Algebra M))
    (hW : ∀ g t x, (W (g * t) x : Algebra M) =
      (W g x : Algebra M) * (W t (shift g x) : Algebra M))
    (hWmeas : ∀ t, AEStronglyMeasurable
      (fun p : D × D => J ((W t p.1 : Algebra M) * star (W t p.2 : Algebra M))) μ)
    {r : ℝ} (hr0 : 0 ≤ r) (hr : r < 1)
    (hnear : ∀ t x y, ‖(W t x : Algebra M) * star (W t y : Algebra M) - 1‖ ≤ r) :
    ∃ (c : D → D → Algebra M) (a : D → D → unitary (Algebra M)),
      AEStronglyMeasurable (fun p : D × D => J (c p.1 p.2)) μ ∧
      (∀ x y, ‖c x y‖ ≤ 1 ∧ ‖c x y - 1‖ ≤ r ∧ IsUnit (c x y) ∧
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.exists_concrete_measurable_diagonal_polar_data line 364

Source documentation

The measurable diagonal construction in the canonical separable trace Hilbert space of a separably acting finite factor.

theorem exists_concrete_measurable_diagonal_polar_data
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    {G D : Type*} [Group G] [Countable G] [MeasurableSpace D] {μ : Measure (D × D)}
    (shift : G → D → D) (W : G → D → unitary (Algebra M))
    (hW : ∀ g t x, (W (g * t) x : Algebra M) =
      (W g x : Algebra M) * (W t (shift g x) : Algebra M))
    (hWmeas : ∀ t, AEStronglyMeasurable (fun p : D × D =>
      concreteTraceEmbedding hM ((W t p.1 : Algebra M) * star (W t p.2 : Algebra M))) μ)
    {r : ℝ} (hr0 : 0 ≤ r) (hr : r < 1)
    (hnear : ∀ t x y, ‖(W t x : Algebra M) * star (W t y : Algebra M) - 1‖ ≤ r) :
    ∃ (c : D → D → Algebra M) (a : D → D → unitary (Algebra M)),
      AEStronglyMeasurable (fun p : D × D => concreteTraceEmbedding hM (c p.1 p.2)) μ ∧
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.concreteTraceEmbedding