OAI/Geometry/SmoothYau/Smoothness/NormIteratedFDerivCompLinear.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.realWaveJet line 44
  2. lemma OAI.YauCounterexamples.realWaveJet_add line 49
  3. lemma OAI.YauCounterexamples.realWaveJet_sum line 55
  4. lemma OAI.YauCounterexamples.fderiv_re_const_mul line 63
  5. lemma OAI.YauCounterexamples.realWaveJet_re_const_mul line 69
  6. lemma OAI.YauCounterexamples.realWaveJet_three line 83
  7. lemma OAI.YauCounterexamples.realWaveJet_comp_bound line 93
  8. def OAI.YauCounterexamples.finiteWaveSuperposition line 169
  9. lemma OAI.YauCounterexamples.contDiff_finiteWaveSuperposition line 173
  10. lemma OAI.YauCounterexamples.realWaveJet_finiteWaveSuperposition line 181
  11. theorem OAI.YauCounterexamples.finite_superposition_pullback_smallBall line 197
  12. lemma OAI.YauCounterexamples.norm_iteratedFDeriv_real_complex_mul line 268
  13. lemma OAI.YauCounterexamples.norm_iteratedFDeriv_finiteWaveSum line 278
  14. theorem OAI.YauCounterexamples.finiteWaveSum_derivative_bound line 295
  15. lemma OAI.YauCounterexamples.normalized_scalar_derivative_bound line 353
  16. lemma OAI.YauCounterexamples.normalized_scalar_lipschitz line 384
  17. lemma OAI.YauCounterexamples.norm_fderiv_evaluation line 397
  18. theorem OAI.YauCounterexamples.realWaveJet_lipschitz_of_relative_bounds line 408
  19. lemma OAI.YauCounterexamples.normalized_scalar_lipschitz_on line 479
  20. theorem OAI.YauCounterexamples.realWaveJet_lipschitz_of_relative_bounds_on line 492
  21. lemma OAI.YauCounterexamples.norm_iteratedFDeriv_comp_linear line 562
  22. lemma OAI.YauCounterexamples.physical_packet_low_derivative line 574
  23. theorem OAI.YauCounterexamples.finiteWaveSuperposition_relative_derivative line 587
  24. theorem OAI.YauCounterexamples.finiteWaveSuperposition_normalized_lipschitz line 614