OAI/Analysis/FourierLLogL/Paths/Letters.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

The uniform output path

  1. abbrev OAI.FourierLLogL.Dyadic.Procedure.Paths.Vector line 16
  2. def OAI.FourierLLogL.Dyadic.Procedure.Paths.dye line 18
  3. def OAI.FourierLLogL.Dyadic.Procedure.Paths.matter line 19
  4. def OAI.FourierLLogL.Dyadic.Procedure.Paths.letter line 20
  5. def OAI.FourierLLogL.Dyadic.Procedure.Paths.shell line 22
  6. def OAI.FourierLLogL.Dyadic.Procedure.Paths.factor line 23
  7. def OAI.FourierLLogL.Dyadic.Procedure.Paths.gain line 25
  8. def OAI.FourierLLogL.Dyadic.Procedure.Paths.fax line 27
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.matter_nonneg line 29
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.matter_sum line 31
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.matter_norm line 33
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.scalar_label line 35
  13. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.scalar_norm line 38
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.matter_split line 42
  15. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.letter_split line 46
  16. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.scalar_split' line 50
  17. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.matter_jump line 54
  18. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.symmetric_curl line 60
  19. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.letter_jump line 67
  20. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.scalar_jump line 70
  21. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.matter_drain line 74
  22. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.scalar_drain line 88
  23. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.shell_abs line 94
  24. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.norm_halfcomplex line 102
  25. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.factor_norm line 106
  26. def OAI.FourierLLogL.Dyadic.Procedure.Paths.billFax line 112
  27. def OAI.FourierLLogL.Dyadic.Procedure.Paths.fullFax line 113
  28. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.fax_floor line 115
  29. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.trip_fax line 119
  30. def OAI.FourierLLogL.Dyadic.Procedure.Paths.proceeds line 123

    Source documentation

    Normalized scalar transform along part (plateau jumps) on path x.

    def proceeds (x u : Grid M) (b : Beat M) :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Grid

  31. def OAI.FourierLLogL.Dyadic.Procedure.Paths.duties line 125
  32. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.gain_series line 128
  33. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.gain_norm line 130