OAI/Analysis/FourierLLogL/Dyadic/Lift.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FourierLLogL.Dyadic.expU_mono line 13
2. lemma OAI.FourierLLogL.Dyadic.avg_mono line 17
3. lemma OAI.FourierLLogL.Dyadic.atom_volume_real line 25
4. def OAI.FourierLLogL.Dyadic.liftGrid line 32

   Source documentation

   Cell averages from the real model.

   def liftGrid (M : ℕ) (f : ℝ → E) (y : Grid M) : E :=
   …

   Mentions: OAI.FourierLLogL.Dyadic.Grid

5. lemma OAI.FourierLLogL.Dyadic.expU_liftGrid line 35
6. lemma OAI.FourierLLogL.Dyadic.liftGrid_ind line 44
7. lemma OAI.FourierLLogL.Dyadic.avg_liftGrid line 57
8. lemma OAI.FourierLLogL.Dyadic.avg_smulHi_lift line 64
9. lemma OAI.FourierLLogL.Dyadic.norm_expU_le line 83
10. lemma OAI.FourierLLogL.Dyadic.norm_avg_le line 88
11. lemma OAI.FourierLLogL.Dyadic.avg_sub line 96
12. lemma OAI.FourierLLogL.Dyadic.liftGrid_const line 103
13. lemma OAI.FourierLLogL.Dyadic.avg_const line 109
14. lemma OAI.FourierLLogL.Dyadic.lift_bounds line 120
15. lemma OAI.FourierLLogL.Dyadic.lift_shift line 133
16. lemma OAI.FourierLLogL.Dyadic.lift_mod_error line 155
17. lemma OAI.FourierLLogL.Dyadic.FinJump_error line 199
18. lemma OAI.FourierLLogL.Dyadic.FinShift_error line 209
19. lemma OAI.FourierLLogL.Dyadic.usable_transfer line 223
20. lemma OAI.FourierLLogL.Dyadic.expU_add_one line 236
21. theorem OAI.FourierLLogL.Dyadic.GridBound.unitTreeBound line 242