OAI/Analysis/Triangular/Taylor/WaveFunction.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AtomicTriangular.Construction.wavePhaseFunction line 13
  2. def OAI.AtomicTriangular.Construction.waveAmplitudeFunction line 16
  3. lemma OAI.AtomicTriangular.Construction.wavePhaseFunction_apply line 18
  4. lemma OAI.AtomicTriangular.Construction.waveAmplitudeFunction_apply line 21
  5. def OAI.AtomicTriangular.Construction.waveFunctionJet line 25
  6. lemma OAI.AtomicTriangular.Construction.waveFunctionJet_apply line 27
  7. lemma OAI.AtomicTriangular.Construction.hasDerivAt_waveFunctionJet line 32
  8. lemma OAI.AtomicTriangular.Construction.differentiable_waveFunctionJet line 38
  9. lemma OAI.AtomicTriangular.Construction.norm_finiteWaveJet_two line 41
  10. lemma OAI.AtomicTriangular.Construction.waveFunctionJet_uniform line 45
  11. def OAI.AtomicTriangular.Construction.inputJJet line 53
  12. def OAI.AtomicTriangular.Construction.pairJJet line 55
  13. def OAI.AtomicTriangular.Construction.pairJ line 57
  14. lemma OAI.AtomicTriangular.Construction.hasDerivAt_inputJJet line 58
  15. lemma OAI.AtomicTriangular.Construction.hasDerivAt_pairJJet line 62
  16. lemma OAI.AtomicTriangular.Construction.pairJJet_iterated line 65
  17. lemma OAI.AtomicTriangular.Construction.pairJ_contDiff line 72