OAI/Combinatorics/TriangleRemoval/Asymptotics/ActiveL2Map.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpTerminalLeave.activeL2Map line 13
  2. def OAI.SharpTerminalLeave.activeL2 line 19
  3. lemma OAI.SharpTerminalLeave.activeL2_sq line 22
  4. lemma OAI.SharpTerminalLeave.activeL2_congr line 28
  5. lemma OAI.SharpTerminalLeave.activeL2_mono line 38
  6. lemma OAI.SharpTerminalLeave.activeL2_coordinate line 45
  7. lemma OAI.SharpTerminalLeave.activeL2_of_bound line 52
  8. lemma OAI.SharpTerminalLeave.movingStar_euler_activeL2 line 70
  9. lemma OAI.SharpTerminalLeave.movingStar_activeL2_bound line 79
  10. lemma OAI.SharpTerminalLeave.movingStarMean_add line 93
  11. lemma OAI.SharpTerminalLeave.movingStarLift_add line 98
  12. theorem OAI.SharpTerminalLeave.movingStar_trajectory_l2_bound line 104
  13. def OAI.SharpTerminalLeave.activeLinf line 172
  14. lemma OAI.SharpTerminalLeave.activeLinf_coordinate line 175
  15. lemma OAI.SharpTerminalLeave.activeLinf_bound line 180
  16. lemma OAI.SharpTerminalLeave.activeLinf_le_l2 line 184
  17. lemma OAI.SharpTerminalLeave.activeL2_le_card_linf line 188
  18. def OAI.SharpTerminalLeave.trajectorySeminorm line 192
  19. lemma OAI.SharpTerminalLeave.trajectorySeminorm_at line 196
  20. lemma OAI.SharpTerminalLeave.trajectorySeminorm_bound line 202
  21. lemma OAI.SharpTerminalLeave.trajectory_mixed_seminorms line 209
  22. def OAI.SharpTerminalLeave.movingStarSolve line 224
  23. lemma OAI.SharpTerminalLeave.movingStarMean_smul line 232
  24. lemma OAI.SharpTerminalLeave.movingStarLift_smul line 239
  25. lemma OAI.SharpTerminalLeave.movingStarSolve_add line 245
  26. lemma OAI.SharpTerminalLeave.movingStarSolve_smul line 265
  27. def OAI.SharpTerminalLeave.movingStarResponse line 283
  28. lemma OAI.SharpTerminalLeave.movingStarResponse_linf line 290
  29. lemma OAI.SharpTerminalLeave.movingStarResponse_l2 line 315