OAI/Analysis/SignedDisk/DirectionNeighbors1.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Actual fixed palette and literal cone coordinates.

  1. lemma OAI.SignedDisk.DirectionNeighbors.scale_scale line 32
  2. lemma OAI.SignedDisk.DirectionNeighbors.shifted_mass_bound line 36
  3. theorem OAI.SignedDisk.DirectionNeighbors.neighbor_energy_budget line 54
  4. def OAI.SignedDisk.ConeCoordinates.axis line 83
  5. def OAI.SignedDisk.ConeCoordinates.coordinate line 84
  6. lemma OAI.SignedDisk.ConeCoordinates.sqrt3_pos line 87
  7. lemma OAI.SignedDisk.ConeCoordinates.sqrt3_sq line 88
  8. lemma OAI.SignedDisk.ConeCoordinates.sqrt3_bounds line 89
  9. lemma OAI.SignedDisk.ConeCoordinates.inner_re line 93
  10. lemma OAI.SignedDisk.ConeCoordinates.inner_im line 96
  11. lemma OAI.SignedDisk.ConeCoordinates.mul_star_of_unit line 99
  12. lemma OAI.SignedDisk.ConeCoordinates.coordinate_apply line 101
  13. lemma OAI.SignedDisk.ConeCoordinates.expansion line 106
  14. lemma OAI.SignedDisk.ConeCoordinates.axis_norm line 114
  15. lemma OAI.SignedDisk.ConeCoordinates.inner_axis line 126
  16. lemma OAI.SignedDisk.ConeCoordinates.coordinate_norm_le line 129
  17. def OAI.SignedDisk.ConeCoordinates.Good line 146

    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.SignedDisk.ConeCoordinates.coordinate

  18. lemma OAI.SignedDisk.ConeCoordinates.good_of_close line 148
  19. lemma OAI.SignedDisk.ConeCoordinates.inner_quarter_self line 174
  20. lemma OAI.SignedDisk.ConeCoordinates.axes_inner line 177
  21. lemma OAI.SignedDisk.ConeCoordinates.norm_le_coords line 186
  22. theorem OAI.SignedDisk.ConeCoordinates.cone_algebra line 192
  23. structure OAI.SignedDisk.ConeCoordinates.Palette line 223

    Source documentation

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

    structure Palette where
…
  24. lemma OAI.SignedDisk.ConeCoordinates.exists_palette line 228
  25. def OAI.SignedDisk.ConeCoordinates.fixedPalette line 243
  26. def OAI.SignedDisk.ConeCoordinates.quantize line 245
  27. lemma OAI.SignedDisk.ConeCoordinates.quantize_close line 247
  28. def OAI.SignedDisk.ActualMarkTrees.tree line 255
  29. lemma OAI.SignedDisk.ActualMarkTrees.vector_tree line 259
  30. lemma OAI.SignedDisk.ActualMarkTrees.terminalMass_tree line 273
  31. lemma OAI.SignedDisk.ActualMarkTrees.sum_terminalMass line 288
  32. lemma OAI.SignedDisk.ActualMarkTrees.vector_actual line 294
  33. theorem OAI.SignedDisk.ActualMarkTrees.mark_budget line 304

    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.SignedDisk.ActualMarkTrees.tree

  34. lemma OAI.SignedDisk.ScalarCancellation.roots_nonneg_of_mass line 322
  35. lemma OAI.SignedDisk.ConeScalar.scalar_integrable line 340
  36. lemma OAI.SignedDisk.ConeScalar.scalar_support line 342
  37. lemma OAI.SignedDisk.ConeScalar.scalar_mass line 346
  38. lemma OAI.SignedDisk.ConeScalar.coordinate_mass_nonneg line 351
  39. lemma OAI.SignedDisk.ConeScalar.good_root_nonneg line 359
  40. lemma OAI.SignedDisk.ConeScalar.root_mass_norm line 370
  41. lemma OAI.SignedDisk.ConeScalar.root_vector_integrable line 379
  42. lemma OAI.SignedDisk.ConeScalar.root_bound line 384
  43. lemma OAI.SignedDisk.ConeScalar.pair_cone line 394