OAI/Analysis/SignedDisk/DyadicHats3.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedDisk.DyadicHats.coeff_eq_hat line 32
2. lemma OAI.SignedDisk.DyadicHats.hat_refine_grid_at line 53
3. lemma OAI.SignedDisk.DyadicHats.vectorMass_grid_refine line 64
4. lemma OAI.SignedDisk.DyadicHats.vectorMass_coeff line 85
5. lemma OAI.SignedDisk.DyadicHats.sum_scalarMass_grid_le line 96
6. lemma OAI.SignedDisk.DyadicHats.hat_lower line 103
7. def OAI.SignedDisk.DyadicHats.nearParent line 119
8. lemma OAI.SignedDisk.DyadicHats.nearParent_int_bound line 121
9. lemma OAI.SignedDisk.DyadicHats.nearParent_box line 125
10. lemma OAI.SignedDisk.DyadicHats.nearParent_mem line 134
11. lemma OAI.SignedDisk.DyadicHats.nearParent_hat_lower line 140
12. lemma OAI.SignedDisk.DyadicHats.nearParent_fiber_card line 156
13. def OAI.SignedDisk.DirectionNeighbors.window line 187

    Source documentation

    The complete fixed grid window. No spatial observation enters the choices.

    def window (d : ℕ) (q : ℤ × ℤ) : Finset (ℤ × ℤ) :=
    …

14. lemma OAI.SignedDisk.DirectionNeighbors.self_mem_window line 190
15. lemma OAI.SignedDisk.DirectionNeighbors.mem_window_iff line 194
16. lemma OAI.SignedDisk.DirectionNeighbors.max_exists line 206
17. def OAI.SignedDisk.DirectionNeighbors.maxVertex line 210
18. lemma OAI.SignedDisk.DirectionNeighbors.maxVertex_mem line 212
19. lemma OAI.SignedDisk.DirectionNeighbors.le_maxVertex line 214
20. def OAI.SignedDisk.DirectionNeighbors.chosen line 218
21. def OAI.SignedDisk.DirectionNeighbors.theta line 220
22. def OAI.SignedDisk.DirectionNeighbors.Theta line 222
23. def OAI.SignedDisk.DirectionNeighbors.worstVertex line 224
24. def OAI.SignedDisk.DirectionNeighbors.energy line 227
25. lemma OAI.SignedDisk.DirectionNeighbors.norm_theta line 230
26. lemma OAI.SignedDisk.DirectionNeighbors.energy_nonneg line 232
27. lemma OAI.SignedDisk.DirectionNeighbors.energy_le_four line 233
28. lemma OAI.SignedDisk.DirectionNeighbors.energy_controls line 239
29. lemma OAI.SignedDisk.DirectionNeighbors.worstVertex_near line 245
30. lemma OAI.SignedDisk.DirectionNeighbors.chosen_near line 250
31. lemma OAI.SignedDisk.DirectionNeighbors.worst_chosen_spec line 257

    Source documentation

    The actual chosen neighbor supplies at least the root's mass and is within 500 fine-grid units, precisely the inputs spent by the coarse triangle defect.

    lemma worst_chosen_spec {r : ℝ} (hr : 0 < r) (h : ℂ → ℂ) (q : ℤ × ℤ) :
        scalarMass h r q ≤ scalarMass h r (chosen h r (worstVertex h r q)) ∧
        boxNorm (point r (chosen h r (worstVertex h r q))-point r q) ≤ 500*r := by
    …

    Mentions: OAI.SignedDisk.DirectionNeighbors.chosen, OAI.SignedDisk.DirectionNeighbors.worstVertex

32. lemma OAI.SignedDisk.DirectionNeighbors.vectorMass_mem_grid line 273
33. def OAI.SignedDisk.DirectionNeighbors.coarseDefect line 288

    Source documentation

    The literal triangle defect over twelve positive refinements.

    def coarseDefect (N : ℕ) (h : ℂ → ℂ) (r : ℝ) (d : ℕ) (p : Grid N) : ℝ :=
    …

34. lemma OAI.SignedDisk.DirectionNeighbors.direction_refine line 291
35. lemma OAI.SignedDisk.DirectionNeighbors.coarseDefect_nonneg line 305
36. lemma OAI.SignedDisk.DirectionNeighbors.coarseDefect_sum line 317
37. def OAI.SignedDisk.DirectionNeighbors.parent line 325
38. lemma OAI.SignedDisk.DirectionNeighbors.neighbor_charge line 329

    Source documentation

    The actual maximally differing neighbor spends true vector cancellation, not an independently postulated directional budget.

    lemma neighbor_charge {N : ℕ} {r R : ℝ} (hr : 0 < r) (hR : 0 ≤ R)
        (hN : R/r+1 ≤ (N:ℝ)) {h : ℂ → ℂ} (hh : Integrable h)
        (hs : ∀ y, h y ≠ 0 → ‖y‖ ≤ R) (q : Grid N) :
        scalarMass h r q*energy h r q ≤ 48*coarseDefect N h r 12 (parent N q) := by
    …

    Mentions: OAI.SignedDisk.DirectionNeighbors.energy, OAI.SignedDisk.DirectionNeighbors.coarseDefect, OAI.SignedDisk.DirectionNeighbors.parent

39. lemma OAI.SignedDisk.DirectionNeighbors.parent_fiber_card line 359
40. lemma OAI.SignedDisk.DirectionNeighbors.parent_sum_bound line 373
41. theorem OAI.SignedDisk.DirectionNeighbors.level_energy_budget line 389

    Source documentation

    Uniform one-scale neighbor energy bound by the actual twelve-scale mass drop.

    theorem level_energy_budget {N : ℕ} {r R : ℝ} (hr : 0 < r) (hR : 0 ≤ R)
        (hN : R/r+1 ≤ (N:ℝ)) {h : ℂ → ℂ} (hh : Integrable h)
        (hs : ∀ y, h y ≠ 0 → ‖y‖ ≤ R) :
        (∑ q : Grid N, scalarMass h r q*energy h r q) ≤
          (48*(4097:ℝ)^2)*((∑ q : Grid N, scalarMass h r q)-
            ∑ p : Grid N, scalarMass h (scale r 12) p) := by
    …

    Mentions: OAI.SignedDisk.DirectionNeighbors.energy