OAI/Analysis/DiskMaximal/DirectionEstimates.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

Actual fixed palette and literal cone coordinates.

  1. def OAI.DirectionNeighbors.window line 56

    Source documentation

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

    def window (d : ℕ) (q : ℤ × ℤ) : Finset (ℤ × ℤ) :=
…
  2. lemma OAI.DirectionNeighbors.self_mem_window line 59
  3. lemma OAI.DirectionNeighbors.mem_window_iff line 63
  4. lemma OAI.DirectionNeighbors.max_exists line 75
  5. def OAI.DirectionNeighbors.maxVertex line 79
  6. lemma OAI.DirectionNeighbors.maxVertex_mem line 81
  7. lemma OAI.DirectionNeighbors.le_maxVertex line 83
  8. def OAI.DirectionNeighbors.chosen line 87
  9. def OAI.DirectionNeighbors.theta line 89
  10. def OAI.DirectionNeighbors.Theta line 91
  11. def OAI.DirectionNeighbors.worstVertex line 93
  12. def OAI.DirectionNeighbors.energy line 96
  13. lemma OAI.DirectionNeighbors.norm_theta line 99
  14. lemma OAI.DirectionNeighbors.energy_nonneg line 101
  15. lemma OAI.DirectionNeighbors.energy_le_four line 102
  16. lemma OAI.DirectionNeighbors.energy_controls line 108
  17. lemma OAI.DirectionNeighbors.worstVertex_near line 114
  18. lemma OAI.DirectionNeighbors.chosen_near line 119
  19. lemma OAI.DirectionNeighbors.worst_chosen_spec line 126

    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.DirectionNeighbors.chosen, OAI.DirectionNeighbors.worstVertex

  20. lemma OAI.DirectionNeighbors.vectorMass_mem_grid line 145
  21. def OAI.DirectionNeighbors.coarseDefect line 160

    Source documentation

    The literal triangle defect over twelve positive refinements.

    def coarseDefect (N : ℕ) (h : ℂ → ℂ) (r : ℝ) (d : ℕ) (p : Grid N) : ℝ :=
…
  22. lemma OAI.DirectionNeighbors.direction_refine line 163
  23. lemma OAI.DirectionNeighbors.coarseDefect_nonneg line 177
  24. lemma OAI.DirectionNeighbors.coarseDefect_sum line 189
  25. def OAI.DirectionNeighbors.parent line 197
  26. lemma OAI.DirectionNeighbors.neighbor_charge line 201

    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.DirectionNeighbors.energy, OAI.DirectionNeighbors.coarseDefect, OAI.DirectionNeighbors.parent

  27. lemma OAI.DirectionNeighbors.parent_fiber_card line 231
  28. lemma OAI.DirectionNeighbors.parent_sum_bound line 245
  29. theorem OAI.DirectionNeighbors.level_energy_budget line 261

    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.DirectionNeighbors.energy

  30. lemma OAI.DirectionNeighbors.scale_scale line 280
  31. lemma OAI.DirectionNeighbors.shifted_mass_bound line 284
  32. theorem OAI.DirectionNeighbors.neighbor_energy_budget line 302
  33. def OAI.ConeCoordinates.axis line 331
  34. def OAI.ConeCoordinates.coordinate line 332
  35. lemma OAI.ConeCoordinates.sqrt3_pos line 335
  36. lemma OAI.ConeCoordinates.sqrt3_sq line 336
  37. lemma OAI.ConeCoordinates.sqrt3_bounds line 337
  38. lemma OAI.ConeCoordinates.inner_re line 341
  39. lemma OAI.ConeCoordinates.inner_im line 344
  40. lemma OAI.ConeCoordinates.mul_star_of_unit line 347
  41. lemma OAI.ConeCoordinates.coordinate_apply line 349
  42. lemma OAI.ConeCoordinates.expansion line 354
  43. lemma OAI.ConeCoordinates.axis_norm line 362
  44. lemma OAI.ConeCoordinates.inner_axis line 374
  45. lemma OAI.ConeCoordinates.coordinate_norm_le line 377
  46. def OAI.ConeCoordinates.Good line 394

    Source documentation

    Closed sector between the literal two palette axes.

    def Good (n z : ℂ) : Prop := 0 ≤ coordinate n 1 z ∧ 0 ≤ coordinate n (-1) z

    Mentions: OAI.ConeCoordinates.coordinate

  47. lemma OAI.ConeCoordinates.good_of_close line 396
  48. lemma OAI.ConeCoordinates.inner_quarter_self line 422
  49. lemma OAI.ConeCoordinates.axes_inner line 425
  50. lemma OAI.ConeCoordinates.norm_le_coords line 434
  51. theorem OAI.ConeCoordinates.cone_algebra line 440
  52. structure OAI.ConeCoordinates.Palette line 471

    Source documentation

    A finite fixed palette, all members genuinely on the unit circle.

    structure Palette where
…
  53. lemma OAI.ConeCoordinates.exists_palette line 476
  54. def OAI.ConeCoordinates.fixedPalette line 491
  55. def OAI.ConeCoordinates.quantize line 493
  56. lemma OAI.ConeCoordinates.quantize_close line 495
  57. def OAI.ActualMarkTrees.tree line 503
  58. lemma OAI.ActualMarkTrees.vector_tree line 507
  59. lemma OAI.ActualMarkTrees.terminalMass_tree line 521
  60. lemma OAI.ActualMarkTrees.sum_terminalMass line 536
  61. lemma OAI.ActualMarkTrees.vector_actual line 542
  62. theorem OAI.ActualMarkTrees.mark_budget line 552

    Source documentation

    The actual finite dyadic vector forest satisfies the intrinsic mark budget. The roots, terminal masses and every intermediate vector are their true hat integrals; no abstract mark budget is supplied as a hypothesis.

    theorem mark_budget {N : ℕ} {h : ℂ → ℂ} (hh : Integrable h) (r : ℝ) (k : ℕ)
    {δ : ℝ} (hδ : 0 < δ) :
    (∑ p : Grid N, costWithRoot (1:ℂ) δ
      (tree (fun q : Grid N => vectorMass h r q) k 1 p)) ≤
        (1+2/δ^2)*(∫ y, ‖h y‖) := by
…

    Mentions: OAI.ActualMarkTrees.tree