OAI/Analysis/LipschitzEquivalence/SlotRadii.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LipschitzCounterexample.HilbertSlots.hasSum_parent line 15
  2. abbrev OAI.LipschitzCounterexample.HilbertSlots.SlotDomain line 23
  3. abbrev OAI.LipschitzCounterexample.HilbertSlots.RadiusBlock line 25
  4. def OAI.LipschitzCounterexample.HilbertSlots.aSq line 28
  5. theorem OAI.LipschitzCounterexample.HilbertSlots.aSq_nonneg line 32
  6. theorem OAI.LipschitzCounterexample.HilbertSlots.hasSum_aSq line 37
  7. def OAI.LipschitzCounterexample.HilbertSlots.radiusBlock line 47
  8. theorem OAI.LipschitzCounterexample.HilbertSlots.radiusBlock_norm_sq line 51
  9. def OAI.LipschitzCounterexample.HilbertSlots.radiusSeq line 57
  10. theorem OAI.LipschitzCounterexample.HilbertSlots.radiusSeq_apply line 63
  11. theorem OAI.LipschitzCounterexample.HilbertSlots.radiusSeq_norm_sq line 66
  12. theorem OAI.LipschitzCounterexample.HilbertSlots.radiusSeq_norm_le line 73
  13. def OAI.LipschitzCounterexample.HilbertSlots.radiusCLM line 81
  14. def OAI.LipschitzCounterexample.HilbertSlots.tailCLM line 99
  15. theorem OAI.LipschitzCounterexample.HilbertSlots.tailCLM_apply line 103
  16. theorem OAI.LipschitzCounterexample.HilbertSlots.tail_norm_le line 109
  17. def OAI.LipschitzCounterexample.HilbertSlots.radius line 115
  18. theorem OAI.LipschitzCounterexample.HilbertSlots.radius_nonneg line 117
  19. theorem OAI.LipschitzCounterexample.HilbertSlots.radius_sq line 119
  20. theorem OAI.LipschitzCounterexample.HilbertSlots.radius_zero_sq line 123
  21. theorem OAI.LipschitzCounterexample.HilbertSlots.radius_step line 126
  22. theorem OAI.LipschitzCounterexample.HilbertSlots.radius_antitone line 131
  23. theorem OAI.LipschitzCounterexample.HilbertSlots.radius_tendsto line 137
  24. theorem OAI.LipschitzCounterexample.HilbertSlots.radius_lipschitz line 141