OAI/Dynamics/TriangleBilliards/ReflectedSmoothing.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TriangularBilliards.SmoothPhase line 15
2. def OAI.TriangularBilliards.directS line 18

   Source documentation

   The direct Euclidean convolution term on one copy of the table.

   def directS (Q : Triangle) (ε : ℝ) (f : SmoothPhase → ℂ)
       (b : ZMod 2) (v : Circle) (x : ℂ) : ℂ :=
   …

   Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.SmoothPhase

3. def OAI.TriangularBilliards.reflectedS line 23

   Source documentation

   The opposite-copy contribution after unfolding through wall i.

   def reflectedS (Q : Triangle) (i : Fin 3) (ε : ℝ) (f : SmoothPhase → ℂ)
       (b : ZMod 2) (v : Circle) (x : ℂ) : ℂ :=
   …

   Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.SmoothPhase

4. def OAI.TriangularBilliards.reflectedSmoothing line 31

   Source documentation

   A bounded global extension of the local disk mollifier. Away from vertices, at most one reflected term can contribute. This fact is proved geometrically instead of assuming a chart or an injectivity-radius bound.

   def reflectedSmoothing (Q : Triangle) (ε : ℝ) (f : SmoothPhase → ℂ) : SmoothPhase → ℂ :=
   …

   Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.SmoothPhase

5. lemma OAI.TriangularBilliards.reflectedDirection_involutive line 35
6. lemma OAI.TriangularBilliards.wallReflection_isometry line 40
7. lemma OAI.TriangularBilliards.kernel_wall_pair line 45
8. lemma OAI.TriangularBilliards.kernel_wall_transfer line 50
9. lemma OAI.TriangularBilliards.seamS_equivariant line 55
10. def OAI.TriangularBilliards.Triangle.coordCLM line 68
11. lemma OAI.TriangularBilliards.Triangle.coord_sub line 71
12. def OAI.TriangularBilliards.Triangle.coordinateBound line 75
13. lemma OAI.TriangularBilliards.Triangle.coordinateBound_nonneg line 77
14. lemma OAI.TriangularBilliards.Triangle.coord_norm_le line 80
15. lemma OAI.TriangularBilliards.Triangle.coord_wallReflection line 87
16. lemma OAI.TriangularBilliards.Triangle.coord_small_of_reflected_near line 98
17. lemma OAI.TriangularBilliards.norm_decompose_sq line 110
18. lemma OAI.TriangularBilliards.reflect_distance_le line 117
19. lemma OAI.TriangularBilliards.Triangle.slope_normal_ne_zero line 139
20. lemma OAI.TriangularBilliards.Triangle.dist_le_reflected_dist line 159

    Source documentation

    Reflection through a supporting line can only increase the distance between two points in the closed table. This also controls tip clearance without any injectivity-radius assumption.

    lemma dist_le_reflected_dist (Q : Triangle) (i : Fin 3) {x y : ℂ}
        (hx : x ∈ Q.table) (hy : y ∈ Q.table) :
        ‖x - y‖ ≤ ‖x - wallReflection Q i y‖ := by
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.wallReflection

21. def OAI.TriangularBilliards.Triangle.clearance line 180

    Source documentation

    Exact distance to the three cone tips.

    def clearance (Q : Triangle) (x : ℂ) : ℝ := Metric.infDist x (range Q.vertex)

    Mentions: OAI.TriangularBilliards.Triangle

22. lemma OAI.TriangularBilliards.Triangle.clearance_nonneg line 182
23. lemma OAI.TriangularBilliards.Triangle.clearance_lipschitz line 185
24. lemma OAI.TriangularBilliards.Triangle.clearance_le_add line 188
25. def OAI.TriangularBilliards.SpatiallyZero line 198
26. lemma OAI.TriangularBilliards.directS_zero_near_tips line 201
27. lemma OAI.TriangularBilliards.reflectedS_zero_near_tips line 215
28. lemma OAI.TriangularBilliards.reflectedSmoothing_zero_near_tips line 231
29. def OAI.TriangularBilliards.Triangle.diameterBound line 240
30. lemma OAI.TriangularBilliards.Triangle.diameterBound_nonneg line 242
31. lemma OAI.TriangularBilliards.Triangle.vertex_dist_le_diameterBound line 245
32. lemma OAI.TriangularBilliards.Triangle.reconstruct_difference line 252
33. lemma OAI.TriangularBilliards.Triangle.clearance_of_coords_small_nonneg line 260
34. lemma OAI.TriangularBilliards.Triangle.clearance_of_coords_small line 282
35. def OAI.TriangularBilliards.Triangle.safetyFactor line 289

    Source documentation

    A concrete fixed safety factor depending only on the triangle.

    def safetyFactor (Q : Triangle) : ℝ := 3 * Q.diameterBound * Q.coordinateBound + 1

    Mentions: OAI.TriangularBilliards.Triangle

36. lemma OAI.TriangularBilliards.Triangle.safetyFactor_pos line 291
37. lemma OAI.TriangularBilliards.Triangle.unique_nearby_wall line 297
38. def OAI.TriangularBilliards.spatialSlice line 322

    Source documentation

    Zero extension of a spatial slice; no value at a seam is used.

    def spatialSlice (Q : Triangle) (f : SmoothPhase → ℂ) (b : ZMod 2) (v : Circle) : ℂ → ℂ :=
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.SmoothPhase

39. def OAI.TriangularBilliards.scalarKernelMap line 325
40. lemma OAI.TriangularBilliards.directS_eq_convolution line 328
41. lemma OAI.TriangularBilliards.directS_contDiff line 341
42. lemma OAI.TriangularBilliards.reflectedS_eq_directS line 350
43. lemma OAI.TriangularBilliards.wallReflection_contDiff line 358
44. lemma OAI.TriangularBilliards.reflectedS_contDiff line 365
45. lemma OAI.TriangularBilliards.reflectedSmoothing_contDiff line 375

    Source documentation

    The genuine kernel construction is spatially smooth on every integrable angular slice. No angular regularization, differentiability or boundedness of f is required.

    lemma reflectedSmoothing_contDiff (Q : Triangle) {ε : ℝ} (hε : 0 < ε)
        {f : SmoothPhase → ℂ} {b : ZMod 2} {v : Circle}
        (hf : IntegrableOn (fun y => f ((y, v), b)) Q.table)
        (hfr : ∀ i, IntegrableOn
          (fun y => f ((y, reflectedDirection Q i v), b + 1)) Q.table) :
        ContDiff ℝ ∞ (fun x => reflectedSmoothing Q ε f ((x, v), b)) := by
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.SmoothPhase, OAI.TriangularBilliards.reflectedDirection, OAI.TriangularBilliards.reflectedSmoothing

46. lemma OAI.TriangularBilliards.reflectedS_zero_of_coord line 384
47. lemma OAI.TriangularBilliards.side_other_coord_large line 398
48. lemma OAI.TriangularBilliards.reflectedSmoothing_seam_germ line 419

    Source documentation

    Near every safe open seam, the full finite kernel is exactly its single unfolded two-sheet chart kernel. The assertion holds on a genuine open neighborhood, so all spatial derivatives also glue.

    lemma reflectedSmoothing_seam_germ (Q : Triangle) {i : Fin 3} {q : ℂ}
        (hq : q ∈ Q.side i) {ε : ℝ} (hε : 0 < ε)
        (hsafe : Q.safetyFactor * ε < Q.clearance q)
        (f : SmoothPhase → ℂ) (b : ZMod 2) (v : Circle) :
        ∀ᶠ x in nhds q,
          reflectedSmoothing Q ε f ((wallReflection Q i x, reflectedDirection Q i v), b + 1) =
            reflectedSmoothing Q ε f ((x, v), b) := by
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.SmoothPhase, OAI.TriangularBilliards.reflectedSmoothing, OAI.TriangularBilliards.wallReflection, OAI.TriangularBilliards.reflectedDirection

49. lemma OAI.TriangularBilliards.directS_fderiv line 453
50. lemma OAI.TriangularBilliards.kernel_lintegral line 471
51. lemma OAI.TriangularBilliards.kernel_row_bound line 476
52. lemma OAI.TriangularBilliards.kernel_col_bound line 484
53. lemma OAI.TriangularBilliards.reflected_kernel_row_bound line 492
54. lemma OAI.TriangularBilliards.reflected_kernel_col_bound line 498