OAI/Geometry/PolarProducts/GalerkinBounds.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FourierPolynomial.leftCoeff line 17
  2. def OAI.FourierPolynomial.rightCoeff line 20
  3. def OAI.FourierPolynomial.joinCoeff line 23
  4. theorem OAI.FourierPolynomial.leftCoeff_apply line 28
  5. theorem OAI.FourierPolynomial.rightCoeff_apply line 31
  6. theorem OAI.FourierPolynomial.joinCoeff_inl line 34
  7. theorem OAI.FourierPolynomial.joinCoeff_inr line 37
  8. theorem OAI.FourierPolynomial.norm_joinCoeff_sq line 40
  9. theorem OAI.FourierPolynomial.energy_joinCoeff line 45
  10. theorem OAI.FourierPolynomial.loop_joinCoeff line 51
  11. def OAI.FourierPolynomial.splitEquiv line 57
  12. theorem OAI.FourierPolynomial.splitEquiv_symm line 85
  13. def OAI.FourierPolynomial.positiveScale line 89
  14. theorem OAI.FourierPolynomial.energy_scaled line 94
  15. theorem OAI.FourierPolynomial.action_positive_lower line 117
  16. theorem OAI.FourierPolynomial.cone_scaled_single line 141
  17. theorem OAI.FourierPolynomial.action_cone_upper line 154
  18. theorem OAI.FourierPolynomial.action_cone_far line 171
  19. def OAI.FourierPolynomial.velocityCoeff line 205
  20. theorem OAI.FourierPolynomial.mode_velocityCoeff line 209
  21. theorem OAI.FourierPolynomial.hasDerivAt_loop line 219
  22. theorem OAI.FourierPolynomial.norm_velocityCoeff_critical line 231
  23. theorem OAI.FourierPolynomial.norm_project_grad line 237
  24. theorem OAI.FourierPolynomial.intervalIntegral_eq_average line 254
  25. def OAI.FourierPolynomial.meanAction line 259
  26. theorem OAI.FourierPolynomial.contDiff_meanAction line 262
  27. theorem OAI.FourierPolynomial.critical_action_eq line 268
  28. def OAI.FourierPolynomial.linkRadius line 297
  29. def OAI.FourierPolynomial.linkLevel line 300
  30. theorem OAI.FourierPolynomial.linkRadius_pos line 303
  31. theorem OAI.FourierPolynomial.linkRadius_sq line 308
  32. theorem OAI.FourierPolynomial.linkLevel_pos line 312
  33. theorem OAI.FourierPolynomial.linkLevel_bound line 316
  34. theorem OAI.FourierPolynomial.exists_link_epsilon line 329
  35. theorem OAI.FourierPolynomial.exists_link_far line 341
  36. theorem OAI.FourierPolynomial.finite_critical line 361