OAI/Geometry/PlaneColoring/BoundaryTrace.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.EuclideanFiveColor.support_good_sequence line 11
2. lemma OAI.EuclideanFiveColor.state_support_avoiding_trace line 24
3. lemma OAI.EuclideanFiveColor.avoiding_trace_palette line 53
4. lemma OAI.EuclideanFiveColor.sample_region_ae line 81
5. lemma OAI.EuclideanFiveColor.sampling_near_region line 93
6. lemma OAI.EuclideanFiveColor.weak_limit_zero_on line 110
7. lemma OAI.EuclideanFiveColor.trace_region_palette line 129
8. lemma OAI.EuclideanFiveColor.outer_strip_trace line 182
9. lemma OAI.EuclideanFiveColor.inner_strip_trace line 210
10. lemma OAI.EuclideanFiveColor.binary_strip_rigidity line 248

    Source documentation

    The source local binary rigidity on arbitrary one-sided strips, allowing independent choices of radial side at the two equilateral neighbors.

    lemma binary_strip_rigidity {k : ℕ} {c : ℂ → Fin k} (hc : Measurable c) (hw : WeakColoring k c)
        {a b : Fin k} {U V : Set ℂ} (hU : IsOpen U) (hV : IsOpen V)
        (hUc : ∀ᵐq : ℂ∂volume,q∈U → c q=a ∨ c q=b)
        (hVc : ∀ᵐq : ℂ∂volume,q∈V → c q=a ∨ c q=b)
        {x e : ℂ} (he : ‖e‖=1) {δ : ℝ} (hδ : 0<δ) (bu bv : Bool)
        (hstripU : ∀e' : ℂ,‖e'‖=1 → dist e' e<δ → ∀r : ℝ,
          0<r → |r-1|<δ → (if bu then 1<r else r<1) → x+(r:ℂ)*e'∈U)
        (hstripV : ∀e' : ℂ,‖e'‖=1 → dist e' (e*(Circle.exp (Real.pi/3) : ℂ))<δ → ∀r : ℝ,
          0<r → |r-1|<δ → (if bv then 1<r else r<1) → x+(r:ℂ)*e'∈V) :
        ∃i : Fin k,(i=a ∨ i=b) ∧ ∃η>0,∀e' : ℂ,‖e'‖=1 → dist e' e<η → ∀r : ℝ,
          0<r → |r-1|<η → (if bu then 1<r else r<1) → x+(r:ℂ)*e'∈essentialLocalSet c i := by
    …

    Mentions: OAI.EuclideanFiveColor.WeakColoring, OAI.EuclideanFiveColor.essentialLocalSet

11. lemma OAI.EuclideanFiveColor.binary_strip_palette_rigidity line 280

    Source documentation

    The resulting fixed outsider is actually in the maximal palette on an angular neighborhood, by one-sided radial weak traces.

    lemma binary_strip_palette_rigidity {k : ℕ} (c : ℂ → Fin k) (hc : Measurable c) (hw : WeakColoring k c)
        {a b : Fin k} {U V : Set ℂ} (hU : IsOpen U) (hV : IsOpen V)
        (hUc : ∀ᵐq : ℂ∂volume,q∈U → c q=a ∨ c q=b)
        (hVc : ∀ᵐq : ℂ∂volume,q∈V → c q=a ∨ c q=b)
        {x : ℂ} {t : Angles} {δ : ℝ} (hδ : 0<δ) (bu bv : Bool)
        (hstripU : ∀e' : ℂ,‖e'‖=1 → dist e' (direction t)<δ → ∀r : ℝ,
          0<r → |r-1|<δ → (if bu then 1<r else r<1) → x+(r:ℂ)*e'∈U)
        (hstripV : ∀e' : ℂ,‖e'‖=1 → dist e' (direction t*(Circle.exp (Real.pi/3) : ℂ))<δ → ∀r : ℝ,
          0<r → |r-1|<δ → (if bv then 1<r else r<1) → x+(r:ℂ)*e'∈V) :
        ∃i : Fin k,(i=a ∨ i=b) ∧ ∃A : Set Angles,IsOpen A ∧ t∈A ∧
          ∀ᵐu∂angularMeasure,u∈A → i∈palette c hc x u := by
    …

    Mentions: OAI.EuclideanFiveColor.WeakColoring, OAI.EuclideanFiveColor.Angles, OAI.EuclideanFiveColor.direction, OAI.EuclideanFiveColor.angularMeasure, OAI.EuclideanFiveColor.palette

12. lemma OAI.EuclideanFiveColor.unit_antipodes_of_no_positive line 319

    Source documentation

    If two unit rays can never be simultaneously positive at a generic angle, they are antipodal. This avoids any assumption about multiplicities of ray lines.

    lemma unit_antipodes_of_no_positive {v w : ℂ} (hv : ‖v‖=1) (hw : ‖w‖=1)
        (h : ∀ᵐt∂angularMeasure,¬(0<⟪direction t,v⟫ ∧ 0<⟪direction t,w⟫)) : w= -v := by
    …

    Mentions: OAI.EuclideanFiveColor.angularMeasure, OAI.EuclideanFiveColor.direction

13. lemma OAI.EuclideanFiveColor.four_split_antipodes line 359

    Source documentation

    The source's all-generic split condition already forces opposite edge positions to be actual antipodes; the collinear case is retained.

    lemma four_split_antipodes (v : Fin 4 → ℂ) (hv : ∀i,‖v i‖=1)
        (hsplit : ∀ᵐt∂angularMeasure,∀i,¬(0<⟪direction t,v i⟫ ∧ 0<⟪direction t,v (i+2)⟫)) :
        ∀i,v (i+2)= -v i := by
    …

    Mentions: OAI.EuclideanFiveColor.angularMeasure, OAI.EuclideanFiveColor.direction