OAI/Analysis/DiskMaximal/DirectionLaws.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DyadicHats.step_support line 55
2. def OAI.DyadicHats.weights line 70
3. def OAI.DyadicHats.pieces line 71
4. def OAI.DyadicHats.densityRoot line 73
5. def OAI.DyadicHats.densityError line 75
6. lemma OAI.DyadicHats.pieces_integrable line 78
7. lemma OAI.DyadicHats.refined_eq_density line 81
8. lemma OAI.DyadicHats.densityRoot_integrable line 91
9. lemma OAI.DyadicHats.densityError_integrable line 94
10. lemma OAI.DyadicHats.densityError_zero_mass line 97
11. lemma OAI.DyadicHats.densityRoot_mass line 101
12. lemma OAI.DyadicHats.densityRoot_abs_mass line 108
13. lemma OAI.DyadicHats.density_support line 115
14. def OAI.DyadicHats.densityDefect line 127
15. lemma OAI.DyadicHats.densityError_cost line 132
16. lemma OAI.DyadicHats.densityError_total_cost line 152
17. def OAI.DyadicHats.coeff line 176

    Source documentation

    Coherent refinement coefficients, evaluated by exact positive matrix composition on the finite box. These are not row-stochastic transitions.

    def coeff (N : ℕ) : ℕ → Grid N → Grid N → ℝ
      | 0,p,q => if p=q then 1 else 0
      | d+1,p,q => ∑ a : Grid N, step p a*coeff N d a q

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

18. lemma OAI.DyadicHats.coeff_nonneg line 180
19. lemma OAI.DyadicHats.coeff_column line 185
20. theorem OAI.DyadicHats.density_decomposition line 196

    Source documentation

    All lower-level error densities, with their actual coherent coefficients, reconstruct the genuine coarse hat density exactly.

    theorem density_decomposition {N : ℕ} {r R : ℝ} (hr : 0 < r) (hR : 0 ≤ R)
        (hN : R/r+1 ≤ (N:ℝ)) {h : ℂ → ℝ} (hs : ∀ y, h y ≠ 0 → ‖y‖ ≤ R)
        (k : ℕ) (q : Grid N) (x : ℂ) :
        hat (scale r k) q x*h x = densityRoot N r h k q x+
          ∑ j ∈ range (k+1), ∑ s : Grid N, coeff N (k-j) q s*densityError N r h j s x := by
    …

    Mentions: OAI.DyadicHats.Grid, OAI.DyadicHats.hat, OAI.DyadicHats.scale, OAI.DyadicHats.densityRoot, OAI.DyadicHats.coeff, OAI.DyadicHats.densityError

21. lemma OAI.DyadicHats.terminal_abs_sum line 210
22. lemma OAI.DyadicHats.densityDefect_sum_succ line 222
23. theorem OAI.DyadicHats.densityDefect_budget_eq line 234

    Source documentation

    Exact telescoping of the literal scalar defects, including the finest terminal split. No depth-dependent or terminal remainder is discarded.

    theorem densityDefect_budget_eq {N : ℕ} {r R : ℝ} (hr : 0 < r)
        (hN : R/r+1 ≤ (N:ℝ)) {h : ℂ → ℝ} (hh : Integrable h)
        (hs : ∀ y, h y ≠ 0 → ‖y‖ ≤ R) (n : ℕ) :
        (∑ k ∈ range (n+1), ∑ q : Grid N, densityDefect N r h k q) =
          ((∫ x, |h x|)-(∑ q : Grid N, |∫ x, hat (scale r n) q x*h x|))/2 := by
    …

    Mentions: OAI.DyadicHats.Grid, OAI.DyadicHats.densityDefect, OAI.DyadicHats.hat, OAI.DyadicHats.scale

24. lemma OAI.DyadicHats.densityDefect_nonneg line 249
25. lemma OAI.DyadicHats.densityDefect_budget line 257
26. def OAI.DyadicHats.scalarPrice line 267

    Source documentation

    The common scalar price assigned to a root. The geometric discount is applied at the actual birth scale of each zero-mass error.

    def scalarPrice (N : ℕ) (r : ℝ) (h : ℂ → ℝ) (ρ : ℝ) (k : ℕ) (q : Grid N) : ℝ :=
    …

    Mentions: OAI.DyadicHats.Grid

27. lemma OAI.DyadicHats.scalarPrice_sum line 270
28. lemma OAI.DyadicHats.discount_recurrence line 286
29. lemma OAI.DyadicHats.triangle_discount_bound line 298
30. theorem OAI.DyadicHats.scalarPrice_budget line 320
31. def OAI.DyadicHats.activeIndices line 336
32. lemma OAI.DyadicHats.hat_zero_of_not_active line 339
33. lemma OAI.DyadicHats.activeIndices_card line 350
34. lemma OAI.DyadicHats.summable_weighted_hat line 356
35. def OAI.DyadicHats.interpolate line 363

    Source documentation

    The literal locally finite tent interpolation, indexed by the whole grid.

    def interpolate (r : ℝ) (f : ℤ × ℤ → ℝ) (x : ℂ) : ℝ := ∑' p, hat r p x*f p

    Mentions: OAI.DyadicHats.hat

36. lemma OAI.DyadicHats.interpolate_eq_sum line 365
37. lemma OAI.DyadicHats.interpolate_add line 372
38. lemma OAI.DyadicHats.interpolate_sub line 376
39. lemma OAI.DyadicHats.interpolate_mul_const line 380
40. lemma OAI.DyadicHats.interpolate_const line 383
41. lemma OAI.DyadicHats.interpolate_nonneg line 385
42. lemma OAI.DyadicHats.interpolate_mono line 387
43. lemma OAI.DyadicHats.interpolate_le_const line 391
44. lemma OAI.DyadicHats.interpolate_finset_sum line 394
45. theorem OAI.DyadicHats.interpolate_lipschitz line 402

    Source documentation

    Only eight tents can contribute to a difference of two interpolated values. This is the quantitative global Lipschitz bound with no grid cardinality loss.

    theorem interpolate_lipschitz {r B : ℝ} (hr : 0 < r) (hB : 0 ≤ B)
        {f : ℤ × ℤ → ℝ} (hf : ∀ p, |f p| ≤ B) :
        LipschitzWith (Real.toNNReal (16*B/r)) (interpolate r f) := by
    …

    Mentions: OAI.DyadicHats.interpolate

46. lemma OAI.FiniteLabels.delta_diff_le_one line 436
47. def OAI.FiniteLabels.spatialRow line 441

    Source documentation

    The actual locally finite transition row on the entire spatial grid.

    def spatialRow (old : ι) (target : ℤ × ℤ → ι) (p : ℤ × ℤ → ℝ)
        (hp0 : ∀ z, 0 ≤ p z) (hp1 : ∀ z, p z ≤ 1) (r : ℝ) (x : ℂ) : Law ι where
    …

    Mentions: OAI.FiniteLabels.Law

48. lemma OAI.FiniteLabels.spatialRow_formula line 458
49. lemma OAI.FiniteLabels.spatialRow_component_lipschitz line 463
50. lemma OAI.FiniteLabels.spatialRow_distance line 474
51. lemma OAI.DyadicHats.interpolate_congr_on line 494
52. lemma OAI.DyadicHats.interpolate_mono_on line 502
53. lemma OAI.DyadicHats.hat_vertex_local line 510
54. lemma OAI.DyadicHats.continuous_boxNorm line 518
55. lemma OAI.DyadicHats.local_neighborhood line 521
56. def OAI.DyadicHats.truncate line 526
57. lemma OAI.DyadicHats.truncate_nonneg line 529
58. lemma OAI.DyadicHats.truncate_le line 531
59. lemma OAI.DyadicHats.interpolate_truncate line 534
60. lemma OAI.FiniteLabels.spatialRow_truncate line 547
61. lemma OAI.FiniteLabels.spatialRow_local_distance line 559
62. lemma OAI.FiniteLabels.spatialRow_local_derivative line 572

    Source documentation

    The derivative cost is bounded by the local switched mass, with a constant fixed by the finite palette, rather than by the number of scales or vertices.

    lemma spatialRow_local_derivative (old : ι) (target : ℤ × ℤ → ι) (p : ℤ × ℤ → ℝ)
        (hp0 : ∀ z, 0 ≤ p z) (hp1 : ∀ z, p z ≤ 1) {r B : ℝ} (hr : 0 < r) (hB : 0 ≤ B)
        {q x : ℂ} (hx : boxNorm (x-q) < 199*r)
        (hpB : ∀ z, boxNorm (point r z-q) ≤ 200*r → p z ≤ B) :
        r*∑ j : ι, ‖gradient (fun y => spatialRow old target p hp0 hp1 r y j) x‖ ≤
          16*(Fintype.card ι:ℝ)*B := by
    …

    Mentions: OAI.FiniteLabels.spatialRow

63. def OAI.FiniteLabels.probability line 598
64. def OAI.FiniteLabels.amplitude line 599
65. lemma OAI.FiniteLabels.probability_formula line 601
66. lemma OAI.FiniteLabels.amplitude_nonneg line 605
67. lemma OAI.FiniteLabels.amplitude_le_one line 607
68. lemma OAI.FiniteLabels.probability_nonneg line 608
69. lemma OAI.FiniteLabels.probability_le_one line 609
70. lemma OAI.FiniteLabels.probability_eq_square line 611
71. lemma OAI.FiniteLabels.amplitude_lipschitz line 620
72. lemma OAI.FiniteLabels.probability_compare line 642
73. lemma OAI.FiniteLabels.probability_norm_compare line 652
74. lemma OAI.FiniteLabels.probability_eq_zero line 663
75. lemma OAI.FiniteLabels.probability_lt_one_iff line 667
76. lemma OAI.FiniteLabels.interpolate_const_mul line 690
77. lemma OAI.FiniteLabels.norm_sub_sq_le_four line 694
78. def OAI.FiniteLabels.switchRate line 701
79. lemma OAI.FiniteLabels.switchRate_nonneg line 704
80. lemma OAI.FiniteLabels.switchRate_le_one line 706
81. lemma OAI.FiniteLabels.probability_le_rate_energy line 711

    Source documentation

    The row-rate comparison is produced from the literal quadratic probability and the actual partition of unity, uniformly over all nearby grid vertices.

    lemma probability_le_rate_energy {τ r E : ℝ} (hτ : 0 < τ) (hr : 0 < r)
        (Θ : ℤ × ℤ → ℂ) (n θ q y : ℂ) (hy : boxNorm (y-q) < 199*r)
        (hE : ∀ z, boxNorm (point r z-q) ≤ 200*r → ‖Θ z-θ‖^2 ≤ E)
        (z : ℤ × ℤ) (hz : boxNorm (point r z-q) ≤ 200*r) :
        probability τ ‖n-Θ z‖ ≤ 2*switchRate τ r Θ n y+8*τ⁻¹^2*E := by
    …

    Mentions: OAI.FiniteLabels.probability, OAI.FiniteLabels.switchRate

82. lemma OAI.FiniteLabels.switchRate_local_compare line 728
83. def OAI.FiniteLabels.spatialSwitchRow line 743
84. lemma OAI.FiniteLabels.spatialSwitchRow_local_distance line 748
85. lemma OAI.FiniteLabels.spatialSwitchRow_local_derivative line 760
86. lemma OAI.DyadicHats.hat_at_point line 776
87. lemma OAI.DyadicHats.hat_vertex_bound line 788
88. lemma OAI.DyadicHats.velocity_bound_on_grid line 806
89. lemma OAI.DyadicHats.coeff_eq_hat line 821
90. lemma OAI.DyadicHats.hat_refine_grid_at line 842
91. lemma OAI.DyadicHats.vectorMass_grid_refine line 853
92. lemma OAI.DyadicHats.vectorMass_coeff line 874
93. lemma OAI.DyadicHats.sum_scalarMass_grid_le line 885
94. lemma OAI.DyadicHats.hat_lower line 895
95. def OAI.DyadicHats.nearParent line 911
96. lemma OAI.DyadicHats.nearParent_int_bound line 913
97. lemma OAI.DyadicHats.nearParent_box line 917
98. lemma OAI.DyadicHats.nearParent_mem line 926
99. lemma OAI.DyadicHats.nearParent_hat_lower line 932
100. lemma OAI.DyadicHats.nearParent_fiber_card line 948