OAI/Geometry/PlaneColoring/Rigidity.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EuclideanFiveColor.evenOffset line 9

   Source documentation

   Common unit neighbor for the transverse chord of length t.

   def evenOffset (v : ℂ) (t : ℝ) : ℂ :=
   …

2. lemma OAI.EuclideanFiveColor.norm_even_wing line 11
3. lemma OAI.EuclideanFiveColor.evenOffset_distances line 23
4. lemma OAI.EuclideanFiveColor.continuous_evenOffset line 31
5. lemma OAI.EuclideanFiveColor.evenOffset_zero line 34
6. def OAI.EuclideanFiveColor.transverseDet line 35
7. def OAI.EuclideanFiveColor.transverseFirst line 37
8. def OAI.EuclideanFiveColor.transverseSecond line 39
9. lemma OAI.EuclideanFiveColor.transverse_decompose line 41
10. lemma OAI.EuclideanFiveColor.continuous_transverseFirst line 50
11. lemma OAI.EuclideanFiveColor.continuous_transverseSecond line 53
12. lemma OAI.EuclideanFiveColor.transverseFirst_zero line 56
13. lemma OAI.EuclideanFiveColor.transverseSecond_zero line 57
14. def OAI.EuclideanFiveColor.evenPath line 58
15. lemma OAI.EuclideanFiveColor.evenPath_edges line 62
16. lemma OAI.EuclideanFiveColor.evenPath_local line 84

    Source documentation

    Actual four-unit-edge paths stay inside the prescribed two open sets for all small starting-point and displacement perturbations.

    lemma evenPath_local {U V : Set ℂ} (hU : IsOpen U) (hV : IsOpen V)
        {p v w : ℂ} (hp : p∈U) (hpv : p+v∈V) (hpw : p+w∈V) :
        ∃r>0,∃δ>0,∀q h : ℂ,q∈Metric.ball p r → ‖h‖<δ →
          |transverseFirst v w h|<2 ∧ |transverseSecond v w h|<2 ∧
          (∀i : Fin 5,(q+evenPath v w h i)∈if i.val%2=0 then U else V) := by
    …

    Mentions: OAI.EuclideanFiveColor.transverseFirst, OAI.EuclideanFiveColor.transverseSecond, OAI.EuclideanFiveColor.evenPath

17. lemma OAI.EuclideanFiveColor.local_ae_translation_constant line 124

    Source documentation

    Local invariance for every sufficiently small fixed translation forces local essential constancy. This is the Fubini/shear step of angular-binary-local.

    lemma local_ae_translation_constant {ι : Type*} [MeasurableSpace ι] [MeasurableSingletonClass ι]
        [Countable ι] (c : ℂ → ι) (hc : Measurable c) {p : ℂ} {r δ : ℝ}
        (hr : 0<r) (hδ : 0<δ)
        (hshift : ∀h : ℂ,‖h‖<δ → ∀ᵐq : ℂ∂volume,q∈Metric.ball p r → c (q+h)=c q) :
        ∃s>0,s≤r ∧ ∃i,∀ᵐq : ℂ∂volume,q∈Metric.ball p s → c q=i := by
    …

18. lemma OAI.EuclideanFiveColor.binary_two_edges line 168
19. lemma OAI.EuclideanFiveColor.ae_translated_unit_pair line 171
20. lemma OAI.EuclideanFiveColor.binary_open_local_rigidity line 179

    Source documentation

    Local essential constancy inside two-color open regions, from the source's actual four-edge paths. The directions are genuine unit directions landing in V.

    lemma binary_open_local_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)
        {p v w : ℂ} (hp : p∈U) (hpv : p+v∈V) (hpw : p+w∈V)
        (hv : ‖v‖=1) (hw' : ‖w‖=1) (hd : transverseDet v w≠0) :
        ∃r>0,∃i : Fin k,∀ᵐq : ℂ∂volume,q∈Metric.ball p r → c q=i := by
    …

    Mentions: OAI.EuclideanFiveColor.WeakColoring, OAI.EuclideanFiveColor.transverseDet

21. lemma OAI.EuclideanFiveColor.transverseDet_mul_unit line 213
22. lemma OAI.EuclideanFiveColor.open_two_unit_directions line 226

    Source documentation

    An open set meeting a unit circle contains two nonparallel unit directions from its center. No regularity of the color classes is involved.

    lemma open_two_unit_directions {V : Set ℂ} (hV : IsOpen V) {p v : ℂ}
        (hv : ‖v‖=1) (hpv : p+v∈V) :
        ∃w : ℂ,p+w∈V ∧ ‖w‖=1 ∧ transverseDet v w≠0 := by
    …

    Mentions: OAI.EuclideanFiveColor.transverseDet

23. lemma OAI.EuclideanFiveColor.double_cos_circle line 251
24. lemma OAI.EuclideanFiveColor.radial_unit_contact line 261

    Source documentation

    The unit circle from one endpoint penetrates either prescribed radial side near its equilateral neighbor. This is the constructive version of the source IFT step.

    lemma radial_unit_contact {x e : ℂ} (he : ‖e‖=1) {δ : ℝ} (hδ : 0<δ)
        {V : Set ℂ} (b : Bool)
        (hstrip : ∀e' : ℂ,‖e'‖=1 → dist e' (e*(Circle.exp (Real.pi/3) : ℂ))<δ →
          ∀r : ℝ,0<r → |r-1|<δ → (if b then 1<r else r<1) → x+(r:ℂ)*e'∈V) :
        ∃v : ℂ,‖v‖=1 ∧ (x+e)+v∈V := by
    …

25. def OAI.EuclideanFiveColor.radialSide line 316
26. def OAI.EuclideanFiveColor.polarBox line 317
27. lemma OAI.EuclideanFiveColor.radialSide_connected line 320
28. lemma OAI.EuclideanFiveColor.radialSide_abs line 322
29. lemma OAI.EuclideanFiveColor.mem_radialSide line 325
30. lemma OAI.EuclideanFiveColor.polarBox_connected line 329
31. lemma OAI.EuclideanFiveColor.polarBox_small line 334

    Source documentation

    Arbitrarily small connected polar boxes on either side of a unit circle.

    lemma polarBox_small {x e : ℂ} {b : Bool} {δ : ℝ} (hδ : 0<δ)
        {U W : Set ℂ} (hW : IsOpen W) (hp : x+e∈W)
        (hstrip : ∀e' : ℂ,‖e'‖=1 → dist e' e<δ → ∀r : ℝ,
          0<r → |r-1|<δ → (if b then 1<r else r<1) → x+(r:ℂ)*e'∈U)
        (he : ‖e‖=1) : ∃ε>0,polarBox x e b ε⊆U∩W := by
    …

    Mentions: OAI.EuclideanFiveColor.polarBox

32. lemma OAI.EuclideanFiveColor.polarBox_contains_strip line 368

    Source documentation

    A polar box contains a complete one-sided radial strip, not just selected rays.

    lemma polarBox_contains_strip {x e : ℂ} (he : ‖e‖=1) (b : Bool)
        {ε : ℝ} (hε : 0<ε) : ∃δ>0,∀e' : ℂ,‖e'‖=1 → dist e' e<δ → ∀r : ℝ,
          |r-1|<δ → (if b then 1<r else r<1) → x+(r:ℂ)*e'∈polarBox x e b ε := by
    …

    Mentions: OAI.EuclideanFiveColor.polarBox

33. def OAI.EuclideanFiveColor.essentialLocalSet line 400

    Source documentation

    Points having a fixed essential color on some ambient neighborhood.

    def essentialLocalSet {ι : Type*} (c : ℂ → ι) (i : ι) : Set ℂ :=
    …

34. lemma OAI.EuclideanFiveColor.essentialLocalSet_open line 402
35. lemma OAI.EuclideanFiveColor.essentialLocalSet_disjoint line 406
36. lemma OAI.EuclideanFiveColor.essentialLocalSet_ae line 413
37. lemma OAI.EuclideanFiveColor.connected_local_ae_constant line 418

    Source documentation

    Local essential constancy on a connected set has one global essential value. The connected set need not be open, which permits polar product images directly.

    lemma connected_local_ae_constant {ι : Type*} {c : ℂ → ι} {S : Set ℂ}
        (hS : IsConnected S) (hl : ∀p∈S,∃i,p∈essentialLocalSet c i) :
        ∃i,S⊆essentialLocalSet c i ∧ (∀ᵐq : ℂ∂volume,q∈S → c q=i) := by
    …

    Mentions: OAI.EuclideanFiveColor.essentialLocalSet