OAI/Geometry/TamingCompatibility/Hodge/HodgeScalarJet.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TamingCompatibility.HodgeScalar.F line 14
  2. def OAI.TamingCompatibility.HodgeScalar.inject line 15
  3. lemma OAI.TamingCompatibility.HodgeScalar.inject_apply line 18
  4. def OAI.TamingCompatibility.HodgeScalar.make line 20
  5. lemma OAI.TamingCompatibility.HodgeScalar.make_apply line 21
  6. lemma OAI.TamingCompatibility.HodgeScalar.make_norm_sq line 23
  7. lemma OAI.TamingCompatibility.HodgeScalar.make_derivative line 26
  8. abbrev OAI.TamingCompatibility.HodgeScalar.Jet line 29
  9. def OAI.TamingCompatibility.HodgeScalar.jetComponent line 30
  10. def OAI.TamingCompatibility.HodgeScalar.jet line 34
  11. lemma OAI.TamingCompatibility.HodgeScalar.make_jet_bound line 37
  12. def OAI.TamingCompatibility.HodgeScalar.jetDistribution line 67
  13. lemma OAI.TamingCompatibility.HodgeScalar.jetDistribution_jet line 69
  14. lemma OAI.TamingCompatibility.HodgeScalar.jet_derivative line 72
  15. lemma OAI.TamingCompatibility.HodgeChart.scalar_add line 88
  16. lemma OAI.TamingCompatibility.HodgeChart.scalar_smul line 96
  17. def OAI.TamingCompatibility.HodgeChart.scalarLinear line 103
  18. def OAI.TamingCompatibility.HodgeChart.scalarVectorLinear line 112
  19. lemma OAI.TamingCompatibility.HodgeChart.scalarVectorLinear_eq_make line 114
  20. def OAI.TamingCompatibility.GeometricHilbert.hodgeScalarToJet line 137
  21. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeScalarToJet_bound line 140
  22. def OAI.TamingCompatibility.GeometricHilbert.hodgeEnergyToScalarJet line 154
  23. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeEnergyToScalarJet_smooth line 156
  24. lemma OAI.TamingCompatibility.GeometricHilbert.hodge_energy_scalar_derivative line 160
  25. def OAI.TamingCompatibility.GeometricHilbert.hodgeScalarDistribution line 174
  26. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeScalarDistribution_H1 line 176
  27. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeScalarDistribution_smooth line 193
  28. def OAI.TamingCompatibility.GeometricHilbert.hodgeRawDistribution line 201
  29. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeRawDistribution_H1 line 205