OAI/Analysis/TreePotential/HilbertSum.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

The outer Hilbert sum: full dual description and reflexivity. Finite-height blocks need not be finite dimensional.

  1. abbrev OAI.BoundedTreePotentials.HilbertSum line 17
  2. lemma OAI.BoundedTreePotentials.single_hilbert_upper line 19
  3. def OAI.BoundedTreePotentials.l2Dual line 35
  4. lemma OAI.BoundedTreePotentials.l2Dual_apply line 40
  5. lemma OAI.BoundedTreePotentials.l2Dual_norm_le line 45
  6. lemma OAI.BoundedTreePotentials.l2Dual_single line 51
  7. def OAI.BoundedTreePotentials.dualRestriction line 59
  8. lemma OAI.BoundedTreePotentials.dualRestriction_apply line 63
  9. lemma OAI.BoundedTreePotentials.dualRestriction_sum_sq_le line 68

    Source documentation

    Finite coefficient inequality, obtained using almost norming block vectors. No block dual functional is assumed to attain its norm.

    lemma dualRestriction_sum_sq_le (φ : StrongDual ℝ (HilbertSum E)) (A : Finset I) :
    ∑ i ∈ A, ‖dualRestriction E φ i‖^2 ≤ ‖φ‖^2 := by
…

    Mentions: OAI.BoundedTreePotentials.HilbertSum, OAI.BoundedTreePotentials.dualRestriction

  10. lemma OAI.BoundedTreePotentials.dualRestriction_mem line 101
  11. def OAI.BoundedTreePotentials.dualPieces line 107
  12. lemma OAI.BoundedTreePotentials.dualPieces_norm_le line 110
  13. lemma OAI.BoundedTreePotentials.l2Dual_dualPieces line 115
  14. lemma OAI.BoundedTreePotentials.dualPieces_l2Dual line 123
  15. lemma OAI.BoundedTreePotentials.l2Dual_norm line 131
  16. def OAI.BoundedTreePotentials.l2DualEquiv line 136

    Source documentation

    Isometric dual description of arbitrary outer l2 sums.

    def l2DualEquiv : HilbertSum (fun i => StrongDual ℝ (E i)) ≃ₗᵢ[ℝ]
    StrongDual ℝ (HilbertSum E) :=
…

    Mentions: OAI.BoundedTreePotentials.HilbertSum

  17. def OAI.BoundedTreePotentials.IsReflexive line 146

    Source documentation

    Reflexive means the canonical embedding onto the continuous bidual is surjective, not merely that the space is isomorphic to some Hilbert space.

    def IsReflexive (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] : Prop :=
…
  18. lemma OAI.BoundedTreePotentials.hilbert_reflexive line 153
  19. lemma OAI.BoundedTreePotentials.reflexive_equiv line 169
  20. theorem OAI.BoundedTreePotentials.hilbertSum_reflexive line 187

    Source documentation

    Reflexivity is preserved by the outer Hilbert sum; this proof includes the non-uniformly Hilbert-equivalent blocks used in both path-cost constructions.

    theorem hilbertSum_reflexive {I : Type*} (E : I → Type*)
    [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace ℝ (E i)]
    (hE : ∀ i, IsReflexive (E i)) : IsReflexive (HilbertSum E) := by
…

    Mentions: OAI.BoundedTreePotentials.IsReflexive, OAI.BoundedTreePotentials.HilbertSum

  21. lemma OAI.BoundedTreePotentials.linearBlock_reflexive line 214
  22. abbrev OAI.BoundedTreePotentials.LinearOuter line 217
  23. theorem OAI.BoundedTreePotentials.linearOuter_reflexive line 219