OAI/GroupTheory/Thompson/AnalyticOscillator.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

The concrete square-integrable oscillator

The representatives are (cos (z*w), sin (z*w)) and its parameter derivative w * (-sin (z*w), cos (z*w)). Every passage from a representative to an Lp element uses an almost-everywhere equality.

  1. def OAI.ThompsonNonamenability.Analytic.waveRep line 23
  2. def OAI.ThompsonNonamenability.Analytic.waveDerivRep line 25
  3. theorem OAI.ThompsonNonamenability.Analytic.continuous_waveRep line 27
  4. theorem OAI.ThompsonNonamenability.Analytic.continuous_waveDerivRep line 30
  5. theorem OAI.ThompsonNonamenability.Analytic.waveRep_norm line 34
  6. theorem OAI.ThompsonNonamenability.Analytic.waveDerivRep_norm line 37
  7. theorem OAI.ThompsonNonamenability.Analytic.waveRep_memLp line 40
  8. theorem OAI.ThompsonNonamenability.Analytic.waveDerivRep_memLp line 44
  9. def OAI.ThompsonNonamenability.Analytic.wave line 51

    Source documentation

    The oscillator as an actual equivalence class in L²([0,1]; ℝ²).

    def wave (z : ℝ) : Hilbert := (waveRep_memLp z).toLp (waveRep z)

    Mentions: OAI.ThompsonNonamenability.Analytic.Hilbert, OAI.ThompsonNonamenability.Analytic.waveRep_memLp, OAI.ThompsonNonamenability.Analytic.waveRep

  10. def OAI.ThompsonNonamenability.Analytic.waveDeriv line 54

    Source documentation

    The proposed derivative, independently defined from its concrete representative.

    def waveDeriv (z : ℝ) : Hilbert :=
…

    Mentions: OAI.ThompsonNonamenability.Analytic.Hilbert

  11. theorem OAI.ThompsonNonamenability.Analytic.wave_coeFn line 57
  12. theorem OAI.ThompsonNonamenability.Analytic.waveDeriv_coeFn line 60
  13. theorem OAI.ThompsonNonamenability.Analytic.integral_intervalMeasure line 63
  14. theorem OAI.ThompsonNonamenability.Analytic.integral_cos_intervalMeasure line 68
  15. theorem OAI.ThompsonNonamenability.Analytic.wave_inner line 77
  16. theorem OAI.ThompsonNonamenability.Analytic.wave_norm line 92
  17. theorem OAI.ThompsonNonamenability.Analytic.waveDeriv_norm_sq line 98
  18. theorem OAI.ThompsonNonamenability.Analytic.wave_inner_waveDeriv line 108
  19. theorem OAI.ThompsonNonamenability.Analytic.waveRep_sub_norm_le line 120
  20. theorem OAI.ThompsonNonamenability.Analytic.waveDerivRep_sub_norm_le line 128
  21. theorem OAI.ThompsonNonamenability.Analytic.wave_sub_norm_le line 143
  22. theorem OAI.ThompsonNonamenability.Analytic.waveDeriv_sub_norm_le line 149
  23. theorem OAI.ThompsonNonamenability.Analytic.waveRep_remainder line 156
  24. theorem OAI.ThompsonNonamenability.Analytic.wave_remainder line 171
  25. theorem OAI.ThompsonNonamenability.Analytic.hasDerivAt_wave line 182
  26. theorem OAI.ThompsonNonamenability.Analytic.continuous_wave line 186
  27. theorem OAI.ThompsonNonamenability.Analytic.lipschitzWith_wave line 189
  28. theorem OAI.ThompsonNonamenability.Analytic.lipschitzWith_waveDeriv line 193
  29. theorem OAI.ThompsonNonamenability.Analytic.continuous_waveDeriv line 197