OAI/Analysis/TreePotential/SegmentBasic.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BoundedTreePotentials.Segments.Node line 15
  2. instance OAI.BoundedTreePotentials.Segments.nodeDecidableEq line 17
  3. def OAI.BoundedTreePotentials.Segments.Prefix line 19
  4. lemma OAI.BoundedTreePotentials.Segments.prefix_refl line 21
  5. lemma OAI.BoundedTreePotentials.Segments.Prefix.trans line 22
  6. lemma OAI.BoundedTreePotentials.Segments.Prefix.antisymm line 25
  7. lemma OAI.BoundedTreePotentials.Segments.prefix_chain line 35
  8. def OAI.BoundedTreePotentials.Segments.prefixAt line 44
  9. def OAI.BoundedTreePotentials.Segments.ancestors line 47
  10. lemma OAI.BoundedTreePotentials.Segments.mem_ancestors line 49
  11. structure OAI.BoundedTreePotentials.Segments.Segment line 67
  12. def OAI.BoundedTreePotentials.Segments.Segment.nodes line 74
  13. lemma OAI.BoundedTreePotentials.Segments.Segment.mem_nodes line 76
  14. lemma OAI.BoundedTreePotentials.Segments.Segment.start_mem line 79
  15. lemma OAI.BoundedTreePotentials.Segments.Segment.finish_mem line 81
  16. def OAI.BoundedTreePotentials.Segments.Segment.singleton line 84
  17. lemma OAI.BoundedTreePotentials.Segments.Segment.singleton_nodes line 86
  18. def OAI.BoundedTreePotentials.Segments.Segment.eval line 95
  19. lemma OAI.BoundedTreePotentials.Segments.Segment.eval_zero line 97
  20. lemma OAI.BoundedTreePotentials.Segments.Segment.eval_neg line 98
  21. lemma OAI.BoundedTreePotentials.Segments.Segment.eval_add line 99
  22. lemma OAI.BoundedTreePotentials.Segments.Segment.eval_smul line 101
  23. lemma OAI.BoundedTreePotentials.Segments.Segment.eval_singleton line 103
  24. lemma OAI.BoundedTreePotentials.Segments.Segment.eval_coordinate line 106
  25. def OAI.BoundedTreePotentials.Segments.Incomparable line 114

    Source documentation

    Incomparability is of starts, equivalently of every node in different segments; mere disjointness is not used as a substitute.

    def Incomparable (F : Finset Segment) : Prop :=
…

    Mentions: OAI.BoundedTreePotentials.Segments.Segment

  26. lemma OAI.BoundedTreePotentials.Segments.incomparable_nodes line 117
  27. lemma OAI.BoundedTreePotentials.Segments.incomparable_disjoint line 130
  28. def OAI.BoundedTreePotentials.Segments.IsUnitTest line 138

    Source documentation

    Closed unit tests for the exact incomparable-segment norm.

    def IsUnitTest (g : Node → ℝ) : Prop :=
…

    Mentions: OAI.BoundedTreePotentials.Segments.Node

  29. lemma OAI.BoundedTreePotentials.Segments.unit_zero line 141
  30. lemma OAI.BoundedTreePotentials.Segments.unit_neg line 142
  31. lemma OAI.BoundedTreePotentials.Segments.unit_segment line 146
  32. lemma OAI.BoundedTreePotentials.Segments.unit_coordinate line 152
  33. lemma OAI.BoundedTreePotentials.Segments.unit_coordinate_test line 155
  34. structure OAI.BoundedTreePotentials.Segments.Atom line 176
  35. def OAI.BoundedTreePotentials.Segments.Atom.profile line 184
  36. def OAI.BoundedTreePotentials.Segments.Atom.pairing line 187
  37. lemma OAI.BoundedTreePotentials.Segments.Atom.coeff_bound line 189
  38. lemma OAI.BoundedTreePotentials.Segments.Atom.profile_at line 194
  39. lemma OAI.BoundedTreePotentials.Segments.Atom.profile_missing line 204
  40. lemma OAI.BoundedTreePotentials.Segments.Atom.profile_bound line 210
  41. def OAI.BoundedTreePotentials.Segments.Atom.zero line 218
  42. def OAI.BoundedTreePotentials.Segments.Atom.neg line 219
  43. def OAI.BoundedTreePotentials.Segments.Atom.coordinate line 221
  44. lemma OAI.BoundedTreePotentials.Segments.Atom.zero_profile line 230
  45. lemma OAI.BoundedTreePotentials.Segments.Atom.neg_profile line 231
  46. lemma OAI.BoundedTreePotentials.Segments.Atom.coordinate_profile line 239
  47. lemma OAI.BoundedTreePotentials.Segments.Atom.pairing_sq_le line 246
  48. lemma OAI.BoundedTreePotentials.Segments.Atom.pairing_bound line 254
  49. lemma OAI.BoundedTreePotentials.Segments.Atom.defect line 260

    Source documentation

    The coefficient replacement identity, retaining both nonnegative deficits.

    lemma defect (A : Atom) {g : Node → ℝ} (hg : IsUnitTest g) :
    0 ≤ 1-A.pairing g ∧
    (∑ S ∈ A.family, (A.coeff S-S.eval g)^2) ≤ 2*(1-A.pairing g) ∧
    1-(∑ S ∈ A.family, (S.eval g)^2) ≤ 2*(1-A.pairing g) := by
…

    Mentions: OAI.BoundedTreePotentials.Segments.Atom, OAI.BoundedTreePotentials.Segments.Node, OAI.BoundedTreePotentials.Segments.IsUnitTest