OAI/NumberTheory/CubicMoment/Theta/CubicThetaGlobalGradient.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

An actual L2 gradient vector, obtained by evaluating the differential in an orthonormal frame at the measurable representative. Its norm is intrinsic even though its coordinates use that representative.

  1. abbrev OAI.CubicFirstMoment.CubicThetaTangentIndex line 12
  2. abbrev OAI.CubicFirstMoment.CubicThetaGradient line 13
  3. abbrev OAI.CubicFirstMoment.CubicThetaGradientL2 line 14
  4. def OAI.CubicFirstMoment.cubicThetaSectionGradient line 16
  5. lemma OAI.CubicFirstMoment.cubicThetaSectionGradient_continuous line 19
  6. lemma OAI.CubicFirstMoment.cubicThetaSectionGradient_norm_sq line 31
  7. def OAI.CubicFirstMoment.cubicThetaGradientRepresentative line 37
  8. lemma OAI.CubicFirstMoment.cubicThetaGradientRepresentative_measurable line 40
  9. lemma OAI.CubicFirstMoment.cubicThetaGradientRepresentative_norm line 44
  10. lemma OAI.CubicFirstMoment.cubicThetaGradientRepresentative_memLp line 52
  11. lemma OAI.CubicFirstMoment.cubicThetaSectionFunction_add line 57
  12. lemma OAI.CubicFirstMoment.cubicThetaSectionFunction_smul line 61
  13. lemma OAI.CubicFirstMoment.cubicThetaSectionGradient_add line 65
  14. lemma OAI.CubicFirstMoment.cubicThetaSectionGradient_smul line 75
  15. def OAI.CubicFirstMoment.cubicThetaGlobalGradient line 84