PredualOrder.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

Operator norm geometry for the original existential Banach-predual gap. These statements use only concrete Hilbert operators. They do not identify any predual or prove trace-orbit separability.

theorem OAI.Generator.norm_imaginary_shift_apply_sq line 26

theorem OAI.Generator.selfAdjoint_norm_le_iff_imaginary_shifts line 43

Source documentation

Self-adjointness and a norm bound are characterized by translated norm balls.

theorem selfAdjoint_norm_le_iff_imaginary_shifts (A : H →L[ℂ] H) (C : ℝ) (hC : 0 ≤ C) :
    (IsSelfAdjoint A ∧ ‖A‖ ≤ C) ↔
      ∀ t : ℝ, ‖A + ((t : ℂ)*Complex.I) • 1‖ ≤ Real.sqrt (C^2+t^2) := by
…

theorem OAI.Generator.predual_selfAdjointBall_isClosed line 102

Source documentation

The self-adjoint ball pulled back to the given weak-star dual is closed.

theorem predual_selfAdjointBall_isClosed :
    IsClosed {φ : WeakDual ℂ X |
      IsSelfAdjoint (e (WeakDual.toStrongDual φ)).val ∧ ‖e (WeakDual.toStrongDual φ)‖ ≤ C} := by
…

theorem OAI.Generator.predual_selfAdjointBall_isCompact line 123

Source documentation

The same set is compact without adding continuity of the algebra isometry.

theorem predual_selfAdjointBall_isCompact :
    IsCompact {φ : WeakDual ℂ X |
      IsSelfAdjoint (e (WeakDual.toStrongDual φ)).val ∧ ‖e (WeakDual.toStrongDual φ)‖ ≤ C} := by
…

theorem OAI.Generator.positive_norm_le_iff_real_shift line 142

Source documentation

Positivity on a bounded self-adjoint ball is one more translated norm bound.

theorem positive_norm_le_iff_real_shift (A : H →L[ℂ] H) (C : ℝ) (hC : 0 ≤ C) :
    (A.IsPositive ∧ ‖A‖ ≤ C) ↔
      (IsSelfAdjoint A ∧ ‖A‖ ≤ C ∧ ‖A - (C : ℂ) • 1‖ ≤ C) := by
…

theorem OAI.Generator.predual_positiveBall_isClosed line 176

Source documentation

Positive balls are weak-star closed for the actual given predual.

theorem predual_positiveBall_isClosed :
    IsClosed {φ : WeakDual ℂ X |
      ContinuousLinearMap.IsPositive (e (WeakDual.toStrongDual φ)).val ∧
      ‖e (WeakDual.toStrongDual φ)‖ ≤ C} := by
…

theorem OAI.Generator.predual_positiveBall_isCompact line 200

Source documentation

Banach--Alaoglu compactness for positive operator balls in the given predual.

theorem predual_positiveBall_isCompact :
    IsCompact {φ : WeakDual ℂ X |
      ContinuousLinearMap.IsPositive (e (WeakDual.toStrongDual φ)).val ∧
      ‖e (WeakDual.toStrongDual φ)‖ ≤ C} := by
…

theorem OAI.Generator.predual_zeroInterval_eq line 222

Source documentation

A positive order interval is the intersection of two translated positive balls.

theorem predual_zeroInterval_eq (b : S) :
    {φ : WeakDual ℂ X | 0 ≤ (e (WeakDual.toStrongDual φ)).val ∧
      (e (WeakDual.toStrongDual φ)).val ≤ b.val} =
    {φ : WeakDual ℂ X |
      ContinuousLinearMap.IsPositive (e (WeakDual.toStrongDual φ)).val ∧
      ‖e (WeakDual.toStrongDual φ)‖ ≤ ‖b‖} ∩
    (fun φ : WeakDual ℂ X => StrongDual.toWeakDual (e.symm b) - φ) ⁻¹'
    {φ : WeakDual ℂ X |
      ContinuousLinearMap.IsPositive (e (WeakDual.toStrongDual φ)).val ∧
      ‖e (WeakDual.toStrongDual φ)‖ ≤ ‖b‖} := by
…

theorem OAI.Generator.predual_zeroInterval_isClosed line 250
theorem OAI.Generator.predual_zeroInterval_isCompact line 258

theorem OAI.Generator.predual_orderInterval_eq line 269

Source documentation

Translate an arbitrary interval to one with lower endpoint zero.

theorem predual_orderInterval_eq (a b : S) :
    {φ : WeakDual ℂ X | a.val ≤ (e (WeakDual.toStrongDual φ)).val ∧
      (e (WeakDual.toStrongDual φ)).val ≤ b.val} =
    (fun φ : WeakDual ℂ X => φ - StrongDual.toWeakDual (e.symm a)) ⁻¹'
    {φ : WeakDual ℂ X | 0 ≤ (e (WeakDual.toStrongDual φ)).val ∧
      (e (WeakDual.toStrongDual φ)).val ≤ (b-a).val} := by
…

theorem OAI.Generator.predual_orderInterval_isClosed line 284
theorem OAI.Generator.predual_orderInterval_isCompact line 291

theorem OAI.Generator.predual_antitone_tendsto line 323

Source documentation

A decreasing net converges weak-star to its greatest lower bound in S.

theorem predual_antitone_tendsto (a : I → S) (l : S)
    (hanti : Antitone (fun i => (a i).val))
    (hlower : ∀ i, l.val ≤ (a i).val)
    (hgreatest : ∀ b : S, (∀ i, b.val ≤ (a i).val) → b.val ≤ l.val) :
    Tendsto (fun i => StrongDual.toWeakDual (e.symm (a i))) atTop
      (𝓝 (StrongDual.toWeakDual (e.symm l))) := by
…

theorem OAI.Generator.predual_monotone_tendsto line 349

Source documentation

An increasing net converges weak-star to its least upper bound in S.

theorem predual_monotone_tendsto (a : I → S) (l : S)
    (hmono : Monotone (fun i => (a i).val))
    (hupper : ∀ i, (a i).val ≤ l.val)
    (hleast : ∀ b : S, (∀ i, (a i).val ≤ b.val) → l.val ≤ b.val) :
    Tendsto (fun i => StrongDual.toWeakDual (e.symm (a i))) atTop
      (𝓝 (StrongDual.toWeakDual (e.symm l))) := by
…

theorem OAI.Generator.predual_antitone_tendsto_zero line 375

Source documentation

In particular, decreasing positive nets with infimum zero tend weak-star to zero.

theorem predual_antitone_tendsto_zero (a : I → S)
    (hanti : Antitone (fun i => (a i).val))
    (hpos : ∀ i, 0 ≤ (a i).val)
    (hgreatest : ∀ b : S, (∀ i, b.val ≤ (a i).val) → b.val ≤ 0) :
    Tendsto (fun i => StrongDual.toWeakDual (e.symm (a i))) atTop (𝓝 0) := by
…

def OAI.Generator.predualFunctional line 397
Source documentation
Evaluation by x, made complex-linear in the algebra argument.
```
def predualFunctional (x : X) : StrongDual ℂ S :=
…
```
theorem OAI.Generator.predualFunctional_apply line 411
theorem OAI.Generator.predualFunctional_norm line 414
def OAI.Generator.predualFunctionalIsometry line 429
Source documentation
A conjugate-linear isometric embedding of the actual given predual.
```
def predualFunctionalIsometry : X →ₗᵢ⋆[ℂ] StrongDual ℂ S where
…
```
theorem OAI.Generator.predualFunctional_separates line 436
Source documentation
Given-predual evaluation functionals separate every two algebra elements.
```
theorem predualFunctional_separates (a b : S)
    (h : ∀ x : X, predualFunctional S e x a = predualFunctional S e x b) : a = b := by
…
```
Mentions: OAI.Generator.predualFunctional

theorem OAI.Generator.predualFunctional_antitone_tendsto line 445

Source documentation

The embedded functional preserves decreasing order limits in S.

theorem predualFunctional_antitone_tendsto (x : X) (a : I → S) (l : S)
    (hanti : Antitone (fun i => (a i).val))
    (hlower : ∀ i, l.val ≤ (a i).val)
    (hgreatest : ∀ b : S, (∀ i, b.val ≤ (a i).val) → b.val ≤ l.val) :
    Tendsto (fun i => predualFunctional S e x (a i)) atTop
      (𝓝 (predualFunctional S e x l)) := by
…

Mentions: OAI.Generator.predualFunctional

theorem OAI.Generator.predualFunctional_monotone_tendsto line 456

Source documentation

The embedded functional preserves increasing order limits in S.

theorem predualFunctional_monotone_tendsto (x : X) (a : I → S) (l : S)
    (hmono : Monotone (fun i => (a i).val))
    (hupper : ∀ i, (a i).val ≤ l.val)
    (hleast : ∀ b : S, (∀ i, (a i).val ≤ b.val) → l.val ≤ b.val) :
    Tendsto (fun i => predualFunctional S e x (a i)) atTop
      (𝓝 (predualFunctional S e x l)) := by
…

Mentions: OAI.Generator.predualFunctional

theorem OAI.Generator.predual_order_squeeze_tendsto_zero line 479
theorem OAI.Generator.predualFunctional_order_squeeze_tendsto_zero line 512