OAI/Analysis/SignedDisk/DyadicHats1.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SignedDisk.DyadicHats.point line 29
2. def OAI.SignedDisk.DyadicHats.boxNorm line 30
3. lemma OAI.SignedDisk.DyadicHats.boxNorm_nonneg line 32
4. lemma OAI.SignedDisk.DyadicHats.boxNorm_le_norm line 33
5. lemma OAI.SignedDisk.DyadicHats.norm_le_two_boxNorm line 35
6. lemma OAI.SignedDisk.DyadicHats.boxNorm_add_le line 40
7. lemma OAI.SignedDisk.DyadicHats.boxNorm_neg line 44
8. lemma OAI.SignedDisk.DyadicHats.boxNorm_sub_comm line 45
9. lemma OAI.SignedDisk.DyadicHats.hat_pos_iff line 48
10. lemma OAI.SignedDisk.DyadicHats.hat_ne_zero_iff line 63
11. lemma OAI.SignedDisk.DyadicHats.support_hat_subset line 71
12. lemma OAI.SignedDisk.DyadicHats.hasCompactSupport_hat line 77
13. lemma OAI.SignedDisk.DyadicHats.lipschitz_hat line 83

    Source documentation

    Globally uniform spatial Lipschitz bound for the literal bilinear hats.

    lemma lipschitz_hat {r : ℝ} (hr : 0 < r) (p : ℤ × ℤ) :
        LipschitzWith (Real.toNNReal (2/r)) (hat r p) := by
    …

    Mentions: OAI.SignedDisk.DyadicHats.hat

14. lemma OAI.SignedDisk.DyadicHats.step_locality line 116
15. def OAI.SignedDisk.DyadicHats.children line 147

    Source documentation

    Literal nine-child support of an adjacent dyadic refinement row.

    def children (p : ℤ × ℤ) : Finset (ℤ × ℤ) :=
    …

16. lemma OAI.SignedDisk.DyadicHats.tent_half_zero line 150
17. lemma OAI.SignedDisk.DyadicHats.step_zero_of_not_child line 160
18. lemma OAI.SignedDisk.DyadicHats.hat_refine_finite line 168
19. def OAI.SignedDisk.DyadicHats.vectorMass line 175

    Source documentation

    The vector mass of the actual density, not an abstract additive tree.

    def vectorMass (h : ℂ → ℂ) (r : ℝ) (p : ℤ × ℤ) : ℂ := ∫ y, hat r p y • h y

    Mentions: OAI.SignedDisk.DyadicHats.hat

20. def OAI.SignedDisk.DyadicHats.scalarMass line 177
21. lemma OAI.SignedDisk.DyadicHats.integrable_hat_smul line 179
22. lemma OAI.SignedDisk.DyadicHats.vectorMass_refine line 185
23. lemma OAI.SignedDisk.DyadicHats.scalarMass_le_integral line 196
24. lemma OAI.SignedDisk.DyadicHats.sum_scalarMass_le line 204

    Source documentation

    Any finite set of roots carries at most the total L1 density, uniformly in the scale. This proves the full-grid mass budget once finite support is used.

    lemma sum_scalarMass_le {h : ℂ → ℂ} (hh : Integrable h) (r : ℝ) (S : Finset (ℤ × ℤ)) :
        ∑ p ∈ S, scalarMass h r p ≤ ∫ y, ‖h y‖ := by
    …

    Mentions: OAI.SignedDisk.DyadicHats.scalarMass

25. lemma OAI.SignedDisk.DyadicHats.scalarMass_refine_le line 221
26. def OAI.SignedDisk.DyadicHats.boundedIndices line 229

    Source documentation

    A finite index set that contains every hat meeting a fixed bounded region.

    def boundedIndices (r R : ℝ) : Finset (ℤ × ℤ) :=
    …

27. lemma OAI.SignedDisk.DyadicHats.mem_boundedIndices line 232
28. lemma OAI.SignedDisk.DyadicHats.vectorMass_zero_of_not_index line 257
29. lemma OAI.SignedDisk.DyadicHats.finite_vectorMass_support line 271

    Source documentation

    Compactly supported actual densities have finitely many nonzero vector masses at each positive scale.

    lemma finite_vectorMass_support {h : ℂ → ℂ} (hc : HasCompactSupport h) {r : ℝ} (hr : 0 < r) :
        (Function.support (vectorMass h r)).Finite := by
    …

    Mentions: OAI.SignedDisk.DyadicHats.vectorMass

30. theorem OAI.SignedDisk.LipschitzWith.integral_fderiv_mul_eq_neg line 293

    Source documentation

    Genuine integration by parts for Lipschitz weights and compact Lipschitz potentials. Differentiability is required only almost everywhere, and follows from Rademacher rather than being a new premise.

    theorem integral_fderiv_mul_eq_neg (hf : LipschitzWith L f) (hg : LipschitzWith K g)
        (hgc : HasCompactSupport g) (v : E) :
        (∫ x, fderiv ℝ f x v * g x ∂μ) = -∫ x, fderiv ℝ g x v * f x ∂μ := by
    …

31. theorem OAI.SignedDisk.LipschitzWith.locallyIntegrable_gradient line 306

    Source documentation

    The total gradient version obtained from Riesz and measurable fderiv is locally integrable, including on the nondifferentiability set.

    theorem locallyIntegrable_gradient (hf : LipschitzWith L f) :
        LocallyIntegrable (gradient f) μ := by
    …

32. theorem OAI.SignedDisk.LipschitzWith.integrable_gradient line 317
33. theorem OAI.SignedDisk.LipschitzWith.integral_mul_fderiv_eq_neg line 324
34. def OAI.SignedDisk.DyadicHats.indexBox line 340
35. abbrev OAI.SignedDisk.DyadicHats.Grid line 342
36. lemma OAI.SignedDisk.DyadicHats.parent_in_box line 344
37. lemma OAI.SignedDisk.DyadicHats.grid_step_column line 370

    Source documentation

    Restriction to a finite box retains the exact column normalization of the positive dyadic refinement matrix; it does not normalize its rows.

    lemma grid_step_column (N : ℕ) (q : Grid N) : (∑ p : Grid N, step p q) = 1 := by
    …

    Mentions: OAI.SignedDisk.DyadicHats.Grid, OAI.SignedDisk.DyadicHats.step

38. lemma OAI.SignedDisk.DyadicHats.mem_indexBox_of_le line 378
39. lemma OAI.SignedDisk.DyadicHats.hat_mul_zero_outside line 388
40. lemma OAI.SignedDisk.DyadicHats.density_partition_grid line 398
41. lemma OAI.SignedDisk.DyadicHats.density_refine_grid line 406
42. lemma OAI.SignedDisk.DyadicHats.integrable_hat_mul line 418
43. def OAI.SignedDisk.DyadicHats.scale line 424
44. lemma OAI.SignedDisk.DyadicHats.scale_pos line 425
45. lemma OAI.SignedDisk.DyadicHats.scale_succ line 426
46. lemma OAI.SignedDisk.DyadicHats.le_scale line 430
47. lemma OAI.SignedDisk.DyadicHats.scale_index_bound line 434