OAI/Analysis/FourierLLogL/Thermal/Form.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Thermal forms on the grid

  1. abbrev OAI.FourierLLogL.Dyadic.Thermal.Form line 16

    Source documentation

    coefficient form. Throughout, nonnegativity of the coefficients means 0 ≤ A.

    abbrev Form (M : ℕ) := Grid M → ℝ

    Mentions: OAI.FourierLLogL.Dyadic.Grid

  2. def OAI.FourierLLogL.Dyadic.Thermal.wave line 18
  3. def OAI.FourierLLogL.Dyadic.Thermal.cost line 19
  4. def OAI.FourierLLogL.Dyadic.Thermal.form line 20
  5. lemma OAI.FourierLLogL.Dyadic.Thermal.wave_even line 22
  6. lemma OAI.FourierLLogL.Dyadic.Thermal.wave_comm line 23
  7. lemma OAI.FourierLLogL.Dyadic.Thermal.wave_abs line 24
  8. lemma OAI.FourierLLogL.Dyadic.Thermal.cost_even line 26
  9. lemma OAI.FourierLLogL.Dyadic.Thermal.cost_symm line 27
  10. lemma OAI.FourierLLogL.Dyadic.Thermal.cost_bounds line 28
  11. lemma OAI.FourierLLogL.Dyadic.Thermal.norm_phase_sq line 33
  12. lemma OAI.FourierLLogL.Dyadic.Thermal.norm_phase_add line 41
  13. lemma OAI.FourierLLogL.Dyadic.Thermal.cost_add line 47
  14. lemma OAI.FourierLLogL.Dyadic.Thermal.form_zero line 54
  15. lemma OAI.FourierLLogL.Dyadic.Thermal.form_at_zero line 56
  16. lemma OAI.FourierLLogL.Dyadic.Thermal.form_add line 59
  17. lemma OAI.FourierLLogL.Dyadic.Thermal.form_smul line 62
  18. lemma OAI.FourierLLogL.Dyadic.Thermal.form_sum line 65
  19. lemma OAI.FourierLLogL.Dyadic.Thermal.form_even line 72
  20. lemma OAI.FourierLLogL.Dyadic.Thermal.form_mono line 74
  21. lemma OAI.FourierLLogL.Dyadic.Thermal.form_nonneg line 78
  22. lemma OAI.FourierLLogL.Dyadic.Thermal.form_triangle line 81
  23. def OAI.FourierLLogL.Dyadic.Thermal.boltz line 89
  24. def OAI.FourierLLogL.Dyadic.Thermal.q line 90
  25. lemma OAI.FourierLLogL.Dyadic.Thermal.boltz_even line 92
  26. lemma OAI.FourierLLogL.Dyadic.Thermal.boltz_pos line 93
  27. lemma OAI.FourierLLogL.Dyadic.Thermal.boltz_sum line 94
  28. lemma OAI.FourierLLogL.Dyadic.Thermal.q_even line 98
  29. lemma OAI.FourierLLogL.Dyadic.Thermal.cq line 101
  30. lemma OAI.FourierLLogL.Dyadic.Thermal.q_origin line 104
  31. lemma OAI.FourierLLogL.Dyadic.Thermal.q_origin_pos line 109
  32. lemma OAI.FourierLLogL.Dyadic.Thermal.q_total line 114
  33. lemma OAI.FourierLLogL.Dyadic.Thermal.q_add line 119
  34. lemma OAI.FourierLLogL.Dyadic.Thermal.boltz_series line 126
  35. def OAI.FourierLLogL.Dyadic.Thermal.F line 132
  36. def OAI.FourierLLogL.Dyadic.Thermal.K line 133
  37. lemma OAI.FourierLLogL.Dyadic.Thermal.F_origin line 135
  38. lemma OAI.FourierLLogL.Dyadic.Thermal.F_zero line 136
  39. lemma OAI.FourierLLogL.Dyadic.Thermal.F_mono line 141
  40. lemma OAI.FourierLLogL.Dyadic.Thermal.K_eq line 148
  41. lemma OAI.FourierLLogL.Dyadic.Thermal.K_even line 154
  42. lemma OAI.FourierLLogL.Dyadic.Thermal.K_pos line 156
  43. lemma OAI.FourierLLogL.Dyadic.Thermal.K_total line 158
  44. def OAI.FourierLLogL.Dyadic.Thermal.label line 163

    Source documentation

    Label noise law centered at zero relative to counting measure.

    def label (A : Form M) : Law (Grid M) :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Thermal.Form, OAI.FourierLLogL.Law, OAI.FourierLLogL.Dyadic.Grid

  45. lemma OAI.FourierLLogL.Dyadic.Thermal.label_apply line 168
  46. lemma OAI.FourierLLogL.Dyadic.Thermal.label_pos line 170
  47. lemma OAI.FourierLLogL.Dyadic.Thermal.label_ex line 173
  48. lemma OAI.FourierLLogL.Dyadic.Thermal.label_cx line 177
  49. def OAI.FourierLLogL.Dyadic.Thermal.cred line 181
  50. lemma OAI.FourierLLogL.Dyadic.Thermal.cred_eq line 183
  51. lemma OAI.FourierLLogL.Dyadic.Thermal.cred_ex line 188
  52. lemma OAI.FourierLLogL.Dyadic.Thermal.cred_norm line 192