OAI/Geometry/CylinderCovering/Singular/EdgeOne.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingularEdgeOne.edgeU_eq line 11
  2. lemma OAI.SingularEdgeOne.edgeV_eq line 15
  3. lemma OAI.SingularEdgeOne.ceiling_rescaling line 23
  4. lemma OAI.SingularEdgeOne.physical_speed_rescaling line 28
  5. lemma OAI.SingularEdgeOne.physical_height_square line 34
  6. lemma OAI.SingularEdgeOne.physical_speed_rescaling_sqrt line 38
  7. lemma OAI.SingularEdgeOne.edgeCeiling_level line 45
  8. lemma OAI.SingularEdgeOne.coefficient_rescaling line 50
  9. lemma OAI.SingularEdgeOne.edge_coefficient line 55
  10. lemma OAI.SingularEdgeOne.edge_coefficient_eq_scaled line 61
  11. lemma OAI.SingularEdgeOne.coefficient_at_one line 65
  12. lemma OAI.SingularEdgeOne.edgeA_at_one line 68
  13. lemma OAI.SingularEdgeOne.edgeG_at_one line 69
  14. lemma OAI.SingularEdgeOne.edgeA_continuous line 71
  15. lemma OAI.SingularEdgeOne.edgeG_continuousAt line 72
  16. lemma OAI.SingularEdgeOne.edgeA_limit line 76
  17. lemma OAI.SingularEdgeOne.edgeG_limit line 79
  18. lemma OAI.SingularEdgeOne.right_rpow_tendsto_zero line 82
  19. lemma OAI.SingularEdgeOne.power_isLittleO_power line 88
  20. lemma OAI.SingularEdgeOne.scaled_cutoff_small line 98
  21. lemma OAI.SingularEdgeOne.power_flexibleCutoff line 110
  22. lemma OAI.SingularEdgeOne.flexibleCutoff_congr line 126
  23. lemma OAI.SingularEdgeOne.edgeOne_flexibleCutoff line 139
  24. lemma OAI.SingularEdgeOne.flexibleCutoff_tip_small line 152
  25. lemma OAI.SingularEdgeOne.parameters_imply_cutoff_bound line 158
  26. lemma OAI.SingularEdgeOne.lower_sweep_dictionary line 162
  27. lemma OAI.SingularEdgeOne.upper_sweep_dictionary line 170
  28. lemma OAI.SingularEdgeOne.cone_dictionary line 178
  29. lemma OAI.SingularEdgeOne.ceiling_dictionary line 182
  30. lemma OAI.SingularEdgeOne.edgeA_integral line 189
  31. lemma OAI.SingularEdgeOne.angularEnergy_integral line 203
  32. lemma OAI.SingularEdgeOne.edgeEnergy_polar line 224
  33. lemma OAI.SingularEdgeOne.edgeEnergy_slice_integral line 234
  34. lemma OAI.SingularEdgeOne.edge_radial_integral line 253
  35. lemma OAI.SingularEdgeOne.edgeG_iterated_integral line 274
  36. lemma OAI.SingularEdgeOne.coefficient_neg line 291
  37. lemma OAI.SingularEdgeOne.edge_coefficient_neg line 301
  38. lemma OAI.SingularEdgeOne.four_rpow_five_halves line 306
  39. lemma OAI.SingularEdgeOne.exact_padding_dictionary line 312
  40. lemma OAI.SingularEdgeOne.exact_cutoff_dictionary line 316