OAI/Analysis/TreePotential/StartModulus.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundedTreePotentials.Segments.startHead line 15
  2. def OAI.BoundedTreePotentials.Segments.startTail line 19
  3. lemma OAI.BoundedTreePotentials.Segments.startCore_head line 21
  4. lemma OAI.BoundedTreePotentials.Segments.startCore_tail line 25
  5. lemma OAI.BoundedTreePotentials.Segments.startHead_coordinate line 30
  6. lemma OAI.BoundedTreePotentials.Segments.startHead_norm line 36
  7. lemma OAI.BoundedTreePotentials.Segments.startTail_norm line 42
  8. lemma OAI.BoundedTreePotentials.Segments.start_coordinate_bound line 48
  9. lemma OAI.BoundedTreePotentials.Segments.sqrt_segment_constant_le_eight line 52
  10. theorem OAI.BoundedTreePotentials.Segments.segment_start_tail line 62

    Source documentation

    The segment-start squared tail bound with constant 64 and both literal coordinate support hypotheses, using equality of representation norms.

    theorem segment_start_tail {E : Finset Node} (hE : Initial (E : Set Node))
    (p y : StartSpace) (hp : ∀ v,v ∉ E → p.val v=0) (hy : ∀ v ∈ E,y.val v=0) :
    ‖p‖^2+‖y‖^2/64≤(max ‖p+y‖ ‖p-y‖)^2 := by
…

    Mentions: OAI.BoundedTreePotentials.Segments.Node, OAI.BoundedTreePotentials.Segments.Initial, OAI.BoundedTreePotentials.Segments.StartSpace

  11. lemma OAI.BoundedTreePotentials.maximumModulus_lower_bound line 112
  12. lemma OAI.BoundedTreePotentials.maximum_center_perturbation line 127
  13. abbrev OAI.BoundedTreePotentials.Segments.startCoordinate line 144
  14. lemma OAI.BoundedTreePotentials.Segments.startCoordinate_apply line 147
  15. def OAI.BoundedTreePotentials.Segments.startFiniteCoordinates line 150
  16. def OAI.BoundedTreePotentials.Segments.startCoordinateTail line 153
  17. lemma OAI.BoundedTreePotentials.Segments.mem_startCoordinateTail line 157
  18. lemma OAI.BoundedTreePotentials.Segments.start_head_approx line 163
  19. theorem OAI.BoundedTreePotentials.Segments.start_completed_tail_bound line 173

    Source documentation

    The finite-codimensional conclusion for the maximum (not averaged) modulus, at every positive radius.

    theorem start_completed_tail_bound (x : StartSpace) (hx : ‖x‖=1)
    {t ε : ℝ} (ht : 0< t) (hε : 0<ε) :
    ∃ F : ClosedFiniteCodim StartSpace, ∀ y, y ∈ F.space → 1 ≤ ‖y‖ →
      Real.sqrt (1+t^2/64)-1-ε ≤ max ‖x+t • y‖ ‖x-t • y‖-1 := by
…

    Mentions: OAI.BoundedTreePotentials.Segments.StartSpace, OAI.BoundedTreePotentials.ClosedFiniteCodim

  20. theorem OAI.BoundedTreePotentials.Segments.start_maximum_modulus line 210
  21. def OAI.BoundedTreePotentials.Segments.startBoundedPath line 216
  22. def OAI.BoundedTreePotentials.Segments.startCoordinateVector line 217
  23. lemma OAI.BoundedTreePotentials.Segments.startBoundedPath_norm line 219
  24. lemma OAI.BoundedTreePotentials.Segments.startCoordinateVector_apply line 222
  25. lemma OAI.BoundedTreePotentials.Segments.startCoordinateVector_norm line 228
  26. lemma OAI.BoundedTreePotentials.Segments.startBoundedPath_increment line 231
  27. lemma OAI.BoundedTreePotentials.Segments.start_children_weaklyNull line 237
  28. theorem OAI.BoundedTreePotentials.Segments.start_renorming_obstruction line 242
  29. theorem OAI.BoundedTreePotentials.Segments.start_no_equivalent_AUC line 251