OAI/Geometry/PolarProducts/QuadraticAction.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DiagonalQuadratic.diag line 15
  2. theorem OAI.DiagonalQuadratic.diag_apply line 19
  3. def OAI.DiagonalQuadratic.diagCLM line 22
  4. theorem OAI.DiagonalQuadratic.diagCLM_apply line 28
  5. theorem OAI.DiagonalQuadratic.real_inner_eq_sum line 30
  6. theorem OAI.DiagonalQuadratic.inner_diag line 34
  7. theorem OAI.DiagonalQuadratic.self_adjoint line 39
  8. def OAI.DiagonalQuadratic.energy line 44
  9. theorem OAI.DiagonalQuadratic.energy_eq_inner line 46
  10. theorem OAI.DiagonalQuadratic.contDiff_energy line 51
  11. theorem OAI.DiagonalQuadratic.hasGradientAt_energy line 55
  12. theorem OAI.DiagonalQuadratic.gradient_energy line 70
  13. theorem OAI.DiagonalQuadratic.norm_diag_sq line 73
  14. theorem OAI.DiagonalQuadratic.norm_diag_lower line 78
  15. theorem OAI.DiagonalQuadratic.norm_diag_upper line 90
  16. theorem OAI.DiagonalQuadratic.energy_smul line 102
  17. theorem OAI.DiagonalQuadratic.energy_mul line 110
  18. theorem OAI.DiagonalQuadratic.energy_lower line 114
  19. theorem OAI.DiagonalQuadratic.energy_nonpos line 119
  20. theorem OAI.DiagonalQuadratic.energy_single line 123
  21. def OAI.FourierPolynomial.action line 144
  22. theorem OAI.FourierPolynomial.contDiff_action line 147
  23. theorem OAI.FourierPolynomial.hasGradientAt_action line 151
  24. theorem OAI.FourierPolynomial.gradient_action line 163
  25. theorem OAI.FourierPolynomial.potential_nonneg line 168
  26. theorem OAI.FourierPolynomial.integral_energy line 171
  27. theorem OAI.FourierPolynomial.potential_lower line 183
  28. theorem OAI.FourierPolynomial.potential_upper_fourth line 195
  29. theorem OAI.FourierPolynomial.project_add line 221
  30. theorem OAI.FourierPolynomial.project_sub line 233
  31. theorem OAI.FourierPolynomial.loop_diag line 244
  32. theorem OAI.FourierPolynomial.loop_smul line 250
  33. theorem OAI.FourierPolynomial.loop_zero line 253
  34. def OAI.FourierPolynomial.remainderLoop line 266
  35. theorem OAI.FourierPolynomial.remainderLoop_apply line 270
  36. theorem OAI.FourierPolynomial.gradient_action_remainder line 276
  37. theorem OAI.FourierPolynomial.norm_gradient_lower line 288
  38. theorem OAI.FourierPolynomial.gradient_coercive line 305
  39. theorem OAI.FourierPolynomial.critical_norm_bound line 315