OAI/Analysis/FourierLLogL/Dyadic/Node.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FourierLLogL.Dyadic.Node.invlen line 16
2. lemma OAI.FourierLLogL.Dyadic.Node.rinv line 18
3. lemma OAI.FourierLLogL.Dyadic.Node.invlen_ge line 20
4. lemma OAI.FourierLLogL.Dyadic.Node.invlen_pos line 22
5. lemma OAI.FourierLLogL.Dyadic.Node.descale line 24
6. lemma OAI.FourierLLogL.Dyadic.Node.mem_block_iff line 30
7. def OAI.FourierLLogL.Dyadic.Node.idx line 41

   Source documentation

   First grid index in a fitting node.

   def idx (p : Node) (M : ℕ) := p.ix * 2^(M-p.lev)

   Mentions: OAI.FourierLLogL.Dyadic.Node

8. def OAI.FourierLLogL.Dyadic.Node.wid line 42
9. lemma OAI.FourierLLogL.Dyadic.Node.fitting line 44
10. lemma OAI.FourierLLogL.Dyadic.Node.wid_pos line 52
11. def OAI.FourierLLogL.Dyadic.Node.start line 54
12. lemma OAI.FourierLLogL.Dyadic.Node.start_val line 56
13. lemma OAI.FourierLLogL.Dyadic.Node.start_pos line 63
14. lemma OAI.FourierLLogL.Dyadic.Node.start_mem line 68
15. def OAI.FourierLLogL.Dyadic.Node.group line 78

    Source documentation

    Finset of vertices.

    def group (p : Node) (M : ℕ) := (p.block M).toFinset

    Mentions: OAI.FourierLLogL.Dyadic.Node

16. lemma OAI.FourierLLogL.Dyadic.Node.mem_group line 80
17. lemma OAI.FourierLLogL.Dyadic.Node.group_range line 82
18. lemma OAI.FourierLLogL.Dyadic.Node.group_card line 87
19. lemma OAI.FourierLLogL.Dyadic.Node.group_size line 97
20. lemma OAI.FourierLLogL.Dyadic.Node.block_separate line 102
21. lemma OAI.FourierLLogL.Dyadic.Node.block_union line 108
22. lemma OAI.FourierLLogL.Dyadic.Node.group_dis line 111
23. lemma OAI.FourierLLogL.Dyadic.Node.group_union line 116
24. def OAI.FourierLLogL.Dyadic.Node.ok line 119
25. lemma OAI.FourierLLogL.Dyadic.Node.root_ok line 121
26. lemma OAI.FourierLLogL.Dyadic.Node.len_top line 122
27. lemma OAI.FourierLLogL.Dyadic.Node.invlen_top line 123
28. lemma OAI.FourierLLogL.Dyadic.Node.group_top line 124
29. lemma OAI.FourierLLogL.Dyadic.Node.avg_sum line 132

    Source documentation

    Local averages as sums.

    lemma avg_sum {E : Type*} [AddCommMonoid E] [SMul ℝ E] (p : Node)
        (f : Grid M → E) :
        p.avg f = p.len⁻¹ • (side M • ∑ x ∈ p.group M, f x) := by
    …

    Mentions: OAI.FourierLLogL.Dyadic.Node, OAI.FourierLLogL.Dyadic.Grid

30. lemma OAI.FourierLLogL.Dyadic.Node.avg_nonneg line 144
31. lemma OAI.FourierLLogL.Dyadic.Node.avg_split_real line 150
32. lemma OAI.FourierLLogL.Dyadic.Node.avg_split_complex line 154
33. def OAI.FourierLLogL.Dyadic.Node.dice line 160

    Source documentation

    Uniform conditional law on a block (total default law if not fitting).

    def dice (p : Node) (M : ℕ) : Law (Grid M) := (uniform _).condP fun x => x ∈ p.block M

    Mentions: OAI.FourierLLogL.Dyadic.Node, OAI.FourierLLogL.Law, OAI.FourierLLogL.Dyadic.Grid

34. lemma OAI.FourierLLogL.Dyadic.Node.prob_block line 162
35. lemma OAI.FourierLLogL.Dyadic.Node.dice_apply line 170
36. lemma OAI.FourierLLogL.Dyadic.Node.dice_positive line 175
37. lemma OAI.FourierLLogL.Dyadic.Node.avg_ex line 181
38. lemma OAI.FourierLLogL.Dyadic.Node.avg_cx line 189
39. lemma OAI.FourierLLogL.Dyadic.Node.dice_child line 197
40. def OAI.FourierLLogL.Dyadic.Node.below line 206

    Source documentation

    Called branching.

    def below (p q : Node) : Prop := p.lev ≥ q.lev ∧ p.cells ⊆ q.cells

    Mentions: OAI.FourierLLogL.Dyadic.Node

41. lemma OAI.FourierLLogL.Dyadic.Node.below_left line 208
42. lemma OAI.FourierLLogL.Dyadic.Node.below_right line 211
43. lemma OAI.FourierLLogL.Dyadic.Node.below_refl line 215
44. lemma OAI.FourierLLogL.Dyadic.Node.below_trans line 217
45. lemma OAI.FourierLLogL.Dyadic.Node.block_of_below line 220
46. lemma OAI.FourierLLogL.Dyadic.Node.scale_below line 223
47. lemma OAI.FourierLLogL.Dyadic.Node.diam_block line 226