OAI/Analysis/FourierLLogL/Paths/Energies.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FourierLLogL.Dyadic.Procedure.Paths.duet line 16
2. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.duet_zero line 17
3. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.duet_self line 18
4. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.duet_add line 20
5. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.duet_sub line 21
6. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.duet_scale line 22
7. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.duet_limit line 24
8. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.duet_inc line 27
9. def OAI.FourierLLogL.Dyadic.Procedure.Paths.meanV line 31
10. def OAI.FourierLLogL.Dyadic.Procedure.Paths.sun line 32
11. def OAI.FourierLLogL.Dyadic.Procedure.Paths.pierce line 33
12. def OAI.FourierLLogL.Dyadic.Procedure.Paths.nub line 34
13. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.mean_hold line 37
14. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.sun_rays line 49
15. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.sun_energy line 54
16. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.energy_small line 64
17. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.pierce_nonneg line 72
18. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.shell_sq line 75
19. def OAI.FourierLLogL.Dyadic.Procedure.Paths.mist line 82
20. def OAI.FourierLLogL.Dyadic.Procedure.Paths.dew line 84
21. def OAI.FourierLLogL.Dyadic.Procedure.Paths.shower line 86
22. def OAI.FourierLLogL.Dyadic.Procedure.Paths.gust line 87
23. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.mist_nonneg line 89
24. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.mist_low line 91
25. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.dew_nonneg line 94
26. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.shower_nonneg line 97
27. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.mean_shift line 100
28. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.sun_shift line 108
29. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.wet_average line 123
30. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.wet_walk line 134
31. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.matter_max line 139
32. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.norm_scaleC line 145
33. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.nub_innovation line 148
34. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.drain_changes line 166

    Source documentation

    Relating mean and energy at removals.

    lemma drain_changes {s q : Scene M} (h : Ideal s q) (u z) :
        let k := matter s z-matter q z
    …

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Procedure.Paths.Ideal, OAI.FourierLLogL.Dyadic.Procedure.Paths.matter

35. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.energy_drain line 206