OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeGradient.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Actual gradient vectors for C1 sections on the finite prime cover. Their norms are the intrinsic derivative energy already proved invariant.

  1. abbrev OAI.CubicFirstMoment.CubicThetaPrimeGradientL2 line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeC1_differentiable line 15
  3. def OAI.CubicFirstMoment.cubicThetaPrimeSectionGradient line 21
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeSectionGradient_continuous line 25
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeSectionGradient_norm_sq line 36
  6. def OAI.CubicFirstMoment.cubicThetaPrimeGradientRepresentative line 44
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimeGradientRepresentative_measurable line 48
  8. lemma OAI.CubicFirstMoment.cubicThetaPrimeGradientRepresentative_norm_sq line 53
  9. lemma OAI.CubicFirstMoment.cubicThetaPrimeGradientRepresentative_norm line 60
  10. lemma OAI.CubicFirstMoment.cubicThetaPrimeAtkinGradient_memLp line 65
  11. lemma OAI.CubicFirstMoment.cubicThetaPrimeSectionGradient_add line 77
  12. lemma OAI.CubicFirstMoment.cubicThetaPrimeSectionGradient_smul line 90