OAI/Analysis/TreePotential/SegmentDual.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundedTreePotentials.Segments.prefixClosure line 14

    Source documentation

    The finite ancestral closure, not a same-level truncation.

    def prefixClosure (E : Finset Node) : Finset Node := E.biUnion ancestors

    Mentions: OAI.BoundedTreePotentials.Segments.Node, OAI.BoundedTreePotentials.Segments.ancestors

  2. lemma OAI.BoundedTreePotentials.Segments.subset_prefixClosure line 16
  3. lemma OAI.BoundedTreePotentials.Segments.initial_prefixClosure line 20
  4. def OAI.BoundedTreePotentials.Segments.finitelyRestrict line 25
  5. lemma OAI.BoundedTreePotentials.Segments.finitelyRestrict_apply line 31
  6. lemma OAI.BoundedTreePotentials.Segments.pairing_finitelyRestrict line 35
  7. lemma OAI.BoundedTreePotentials.Segments.finitePairing_coeff_smul line 42
  8. lemma OAI.BoundedTreePotentials.Segments.polar_pairing_bound line 49
  9. def OAI.BoundedTreePotentials.Segments.finiteDual line 72

    Source documentation

    On finite arrays this is exactly the coefficient functional in the full dual.

    def finiteDual : (Node →₀ ℝ) →ₗ[ℝ] Dual :=
…

    Mentions: OAI.BoundedTreePotentials.Segments.Node, OAI.BoundedTreePotentials.Segments.Dual

  10. lemma OAI.BoundedTreePotentials.Segments.finiteDual_apply line 75
  11. lemma OAI.BoundedTreePotentials.Segments.finiteDual_lift line 79
  12. lemma OAI.BoundedTreePotentials.Segments.finiteDual_norm_le line 88
  13. lemma OAI.BoundedTreePotentials.Segments.finiteDual_norm line 99
  14. def OAI.BoundedTreePotentials.Segments.finiteDualIsometry line 114
  15. def OAI.BoundedTreePotentials.Segments.coreToDual line 118
  16. lemma OAI.BoundedTreePotentials.Segments.coreToDual_coe line 121
  17. lemma OAI.BoundedTreePotentials.Segments.coreToDual_lift line 126
  18. lemma OAI.BoundedTreePotentials.Segments.coreToDual_norm line 129
  19. def OAI.BoundedTreePotentials.Segments.coreToDualIsometry line 136
  20. lemma OAI.BoundedTreePotentials.Segments.coordinateFunctional_total line 140
  21. lemma OAI.BoundedTreePotentials.Segments.coreToDual_surjective line 163
  22. def OAI.BoundedTreePotentials.Segments.coreDualEquiv line 198

    Source documentation

    The segment estimate extends to the completed dual.

    def coreDualEquiv : DualCore ≃ₗᵢ[ℝ] Dual :=
…

    Mentions: OAI.BoundedTreePotentials.Segments.DualCore, OAI.BoundedTreePotentials.Segments.Dual

  23. theorem OAI.BoundedTreePotentials.dual_reflexive line 206

    Source documentation

    Surjectivity of the canonical bidual map passes to the continuous dual.

    theorem dual_reflexive {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (hE : IsReflexive E) : IsReflexive (StrongDual ℝ E) := by
…

    Mentions: OAI.BoundedTreePotentials.IsReflexive

  24. theorem OAI.BoundedTreePotentials.Segments.incomparable_reflexive line 219
  25. theorem OAI.BoundedTreePotentials.Segments.core_reflexive line 221
  26. def OAI.BoundedTreePotentials.Segments.dualHead line 227

    Source documentation

    Coordinate truncation on the full dual, defined by the biorthogonal basis independently of the core isometry.

    def dualHead (E : Finset Node) : Dual →L[ℝ] Dual :=
…

    Mentions: OAI.BoundedTreePotentials.Segments.Node, OAI.BoundedTreePotentials.Segments.Dual

  27. def OAI.BoundedTreePotentials.Segments.dualTail line 231
  28. lemma OAI.BoundedTreePotentials.Segments.dualHead_apply line 233
  29. lemma OAI.BoundedTreePotentials.Segments.coreToDual_coordinate line 237
  30. lemma OAI.BoundedTreePotentials.Segments.coreToDual_coordinate_apply line 243
  31. lemma OAI.BoundedTreePotentials.Segments.coreToDual_head line 257
  32. lemma OAI.BoundedTreePotentials.Segments.coreToDual_tail line 262
  33. theorem OAI.BoundedTreePotentials.Segments.incomparable_tail line 269

    Source documentation

    Full-dual version of the incomparable-segment estimate, with the exact constant and the literal coordinate head.

    theorem incomparable_tail {E : Finset Node} (hE : Initial (E : Set Node))
    (x y : Dual) (hx : dualHead E x=x) (hp : ‖x+y‖ ≤ 1) (hm : ‖x-y‖ ≤ 1) :
    ‖dualTail E y‖ ≤ (Real.sqrt 2+Real.sqrt 6)*Real.sqrt (1-‖x‖) := by
…

    Mentions: OAI.BoundedTreePotentials.Segments.Node, OAI.BoundedTreePotentials.Segments.Initial, OAI.BoundedTreePotentials.Segments.Dual, OAI.BoundedTreePotentials.Segments.dualHead, OAI.BoundedTreePotentials.Segments.dualTail

  34. lemma OAI.BoundedTreePotentials.completedHead_idem line 287
  35. lemma OAI.BoundedTreePotentials.completedHead_ker line 296
  36. instance OAI.BoundedTreePotentials.completedHead_finiteRank line 308
  37. lemma OAI.BoundedTreePotentials.completedTail_idem line 315
  38. lemma OAI.BoundedTreePotentials.completedHead_tail line 319