generic great circle on the sphere misses any finite set

Stream: Is there code for X?

[Alex Kontorovich]

Do we have something like the following already? I want to know that given any finite set of points on the sphere, there is a great circle that misses all of them... Thanks!

[Ruben Van de Velde]

That sounds like something that might not even be obvious to state. Unless it exists in sphere eversion?

[Adam Topaz]

I assume the sphere is centered in Euclidean space? In that case it could be stated in terms of the intersection of the sphere with some generic hyperplane.

[Richard Copley]

(Does our EuclideanSpace have a center?)

Easy to prove on paper: let $S^2$ be the unit sphere center the origin in the real inner-product space $\mathbb{R}^3$. Let $s$ be a finite set of points of $S^2$.

Choose an antipodal pair $p$, $-p$ of points of $S^2$ [edit: disjoint from $s$] and choose an orthogonal basis $\mathscr{E}$ such that $p = (0, 0, 1)_{\mathscr{E}}$.

Let $t = \{\theta(x) : x \in s\}$, a finite set, where $\theta(x)$ is the azimuth of $x = (\cos\theta\sin\phi, \sin\theta\sin\phi, \cos\phi)_{\mathscr{E}}$ for all $x \in S^2 \setminus \{p, -p\}$.

Choose an angle $\theta \notin t$. Then the great circle is $(\cos\theta\sin\phi, \sin\theta\sin\phi, \cos\phi)_{\mathscr{E}}$ has the desired property.

[Adam Topaz]

Oh, I was thinking that one should prove the more general fact that given a finite set of nonzero points in $\mathbb{R}^n$ (n > 1) you can find some hyperplane which misses them all.

[Richard Copley]

Hmm, ok. Choose an origin [edit: outside the finite set], then do the above (the distance of each of the points considered from the origin is irrelevant).

[Scott Carnahan]

Alternatively, there is a linear functional that doesn't vanish at any of the finitely many points.

[Adam Topaz]

That sounds like something we may actually have...

[Richard Copley]

This is too easy if we're allowed to use any plane (or equivalently, if we desire a subspace but we are allowed to choose the origin): use the plane $x=X$ where $X > x_i$ for all $(x_i, y_i, z_i)\in s$.

[Richard Copley]

@Adam Topaz yep, nonzero points, and a linear subspace, not just a hyperplane

[Adam Topaz]

Yeah of course

[Scott Carnahan]

Another alternative: Finitely many nonzero points describe a finite union of hyperplanes in the dual space, and this is not the whole dual space.

[Adam Topaz]

I think that's probably the best approach for mathlib: prove that over an infinite field a vector space cannot be the union of finitely many proper subspaces (or better, provide a bound on the cardinality of the field given the fact that a vector space is the union of finitely many subspaces). Then use Scott's argument in the dual space, etc.

[Jireh Loreaux]

This works for countably many points too, right?

[Antoine Chambert-Loir]

And if you're willing to be teasing, it even works for $<2^{\aleph_0}$ points.

[Richard Copley]

There's a nice proof here

[Richard Copley]

And there's a not-nice formalization of (the inside bit of) it below. I only did the < ℵ₀ case.

import Mathlib.Tactic

set_option autoImplicit false

variable (𝕜 E : Type*) [RCLike 𝕜] [AddCommGroup E] [inst: Module 𝕜 E]

-- If `s` is a finite set of submodules properly included in the submodule `m`,
-- the union of the submodules in `s` is a proper subset of `m`.
example (n : ℕ) : ∀ m : Submodule 𝕜 E, ⊥ < m → ∀ s : Finset (Submodule 𝕜 E),
    s.card ≤ n → (∀ x ∈ s, x < m) → ¬(m : Set E) ⊆ ⋃ x ∈ s, x := by
  classical
  have h₀ (m : Submodule 𝕜 E) (s : Finset (Submodule 𝕜 E)) (hn : s.card = 0) :
      ¬(m : Set E) ⊆ ⋃ x ∈ s, (x : Set E) := by
    rw [Finset.card_eq_zero.mp hn, Set.not_subset]
    exact ⟨0, zero_mem m, by rw [Set.mem_iUnion₂]; nofun⟩
  induction n with
  | zero =>
    rintro m - s hn -
    exact h₀ m s (Nat.eq_zero_of_le_zero hn)
  | succ n ih =>
    intro m hm s hn hproper
    by_cases h : s.card = 0
    . exact h₀ m s h
    rw [Finset.card_eq_zero, ← ne_eq, ← Finset.nonempty_iff_ne_empty] at h
    have ⟨m', hm'⟩ := h
    by_cases hinc : ∃ y ∈ s.erase m', m' ≤ y
    . have ⟨y, hy, hym'⟩ := hinc
      have herase : (⋃ x ∈ s.erase m', x) = ⋃ x ∈ s, (x : Set E) := by
        conv_rhs => rw [← Finset.insert_erase hm', Finset.set_biUnion_insert]
        rw [← Finset.insert_erase hy, Finset.set_biUnion_insert]
        exact (Set.union_eq_self_of_subset_left (Set.subset_union_of_subset_left hym' _)).symm
      have hcard : (s.erase m').card ≤ n := Finset.card_erase_of_mem hm' ▸ Nat.sub_le_of_le_add hn
      have hlt : ∀ x ∈ s.erase m', x < m := fun x hx => hproper x (Finset.mem_of_mem_erase hx)
      rw [← herase]
      exact ih m hm ((s.erase m')) hcard hlt
    rw [not_exists] at hinc
    by_cases hempty : s.erase m' = ∅
    . obtain rfl : s = {m'} := by
        rw [Finset.nonempty_iff_ne_empty] at h
        rw [Finset.erase_eq_empty_iff] at hempty
        exact hempty.resolve_left h
      rw [Finset.set_biUnion_singleton]
      exact not_subset_of_ssubset (hproper m' hm')
    rw [← ne_eq, ← Finset.nonempty_iff_ne_empty] at hempty
    have ⟨x, hx⟩ := hempty
    have hbot : ⊥ < m' := lt_of_le_of_lt bot_le (inf_lt_right.mpr (not_and.mp (hinc x) hx))
    have hcard : (Finset.image (fun y => y ⊓ m') (s.erase m')).card ≤ n :=
      Finset.card_image_le.trans (Finset.card_erase_of_mem hm' ▸ Nat.sub_le_of_le_add hn)
    specialize ih m' hbot ((s.erase m').image fun y => y ⊓ m') hcard <| by
      intro x hx
      rw [Finset.mem_image] at hx
      obtain ⟨y, hy, rfl⟩ := hx
      exact inf_lt_right.mpr (not_and.mp (hinc y) hy)
    rw [Finset.set_biUnion_finset_image] at ih
    rw [Set.not_subset_iff_exists_mem_not_mem] at ih
    have ⟨u, hum', hu⟩ := ih
    have ⟨v, hvm, hvm'⟩ := (SetLike.lt_iff_le_and_exists.mp (hproper m' hm')).2
    replace hu : ∀ x ∈ s.erase m', u ∉ x := by
      contrapose! hu
      have ⟨y, hy, huy⟩ := hu
      exact Set.subset_iUnion₂_of_subset y hy subset_rfl (Submodule.mem_inf.mpr ⟨huy, hum'⟩)
    have ⟨r, hcard⟩ : ∃ r : Finset 𝕜, n + 1 ≤ r.card := by
      apply Cardinal.exists_finset_le_card
      apply (Cardinal.nat_lt_aleph0 (n + 1)).le.trans
      exact Cardinal.infinite_iff.mp inferInstance
    have ⟨t, _, h⟩ : ∃ t ∈ r, ∀ x ∈ s, v + t • u ∉ x := by
      rw [← not_forall_not]
      intro h
      replace h : ∀ t : r, ∃ x : s.erase m', v + t.val • u ∈ x.val := by
        intro t
        have ⟨x, hx'⟩ := not_forall.mp (not_and.mp (h t.val) t.property)
        rw [← not_and, not_not] at hx'
        have : x ≠ m' := by
          rintro rfl
          apply hvm'
          rw [← Submodule.add_mem_iff_left x (Submodule.smul_mem x (↑t) hum')]
          exact hx'.2
        exact ⟨⟨x, Finset.mem_erase_of_ne_of_mem this hx'.1⟩, hx'.2⟩
      choose g hfg using h
      refine not_lt_of_le ?_ (Nat.add_one_le_iff.mp hcard)
      trans (s.erase m').card
      . rw [← Nat.card_eq_finsetCard, ← Nat.card_eq_finsetCard]
        apply Finite.card_le_of_injective g
        intro t₁ t₂ hg
        rw [Subtype.ext_iff]
        by_contra! ht
        apply hu (g t₁).val (g t₁).property
        rw [← one_smul 𝕜 u, ← inv_mul_cancel (sub_ne_zero_of_ne ht.symm), ← smul_smul]
        apply Submodule.smul_mem
        rw [← Submodule.add_mem_iff_right _ (hfg t₁), sub_smul, add_add_sub_cancel]
        exact hg ▸ hfg t₂
      . exact Finset.card_erase_of_mem hm' ▸ Nat.sub_le_of_le_add hn
    rw [Set.not_subset]
    refine ⟨v + t • u, ?_, ?_⟩
    . exact Submodule.add_mem _ hvm <| Submodule.smul_mem _ t ((hproper m' hm').le hum')
    . rw [Set.mem_iUnion₂, not_exists]
      intro x
      rw [not_exists]
      intro hx
      exact h x hx

[Vincent Beffara]

Another option, fix the big circle but move the points using a uniformly chosen element of SO3, by a union bound you just have to show that one point is moved a.s. to the complement of the circle, which in turn is the statement that the circle has measure 0. (Which also works for countably many points.)

[Antoine Chambert-Loir]

Yet another option: prove that a union of nontrivial polynomial hypersurfaces misses one point. (Works over any infinite field, with strictly less hypersurfaces than the cardinality of the field.)

[Richard Copley]

One can (and should) replace [RCLike 𝕜] with [Field 𝕜] [Infinite 𝕜] in my proof but, as written, it does rely on n : ℕ.

[Richard Copley]

Neither more nor less generally:

import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

open MeasureTheory

variable (E : Type*)
  [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E]
  [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E)
  [μ.IsAddHaarMeasure] in
theorem Submodule.biUnion_countable_ne_top
    (s : Set (Submodule ℝ E)) (hs : s.Countable) (h : ∀ x ∈ s, x < ⊤) :
      ⋃ x ∈ s, x ≠ (Set.univ : Set E) := by
  intro huniv
  apply IsOpen.measure_ne_zero μ isOpen_univ Set.univ_nonempty
  rw [← huniv, measure_biUnion_null_iff hs]
  exact fun x hx => Measure.addHaar_submodule μ x (h x hx).ne

example (n : ℕ) (s : Set (Submodule ℝ (Fin n → ℝ)))
    (hs : s.Countable) (h : ∀ x ∈ s, x < ⊤) :
      ⋃ x ∈ s, x ≠ (Set.univ : Set (Fin n → ℝ)) :=
  Submodule.biUnion_countable_ne_top (Fin n → ℝ) volume s hs h

[Junyan Xu]

The result is also needed to show an algebraic extension of fields is determined by the set of all minimal polynomials. You might try to formalize this more general result if you feel like doing it.

[Richard Copley]

Thanks for the suggestion. There is a WIP PR #13040. The first sub-lemma is proved.

[Antoine Chambert-Loir]

Funnily I had proved the end of the paper. #13047
It seems that if we merge our two PR, only the middle part has to be proved (that the cosets of subgroups of finite index still cover the group).

[Richard Copley]

I have added a commit with the middle part,

/-- Let the group `G` be the union of finitely many left cosets `g i • H i`.
Then the cosets of subgroups of infinite index may be omitted from the covering. -/
theorem Fintype.covers_finiteIndex_of_covers {G ι : Type*} [Group G] [Fintype ι]
    [DecidablePred fun (H : Subgroup G) => H.FiniteIndex]
    (g : ι → G) (H : ι → Subgroup G) (hcovers : ⋃ k, g k • (H k : Set G) = Set.univ) :
    ⋃ k ∈ Finset.univ.filter (fun i => (H i).FiniteIndex), g k • (H k : Set G) = Set.univ := by
  sorry

There is a lot of scope for simplification and golfing, and I wasn't working with your PR in mind, @Antoine Chambert-Loir, so I expect changes will be needed to make the two compatible.

[Antoine Chambert-Loir]

Great! I borrowed your code, added your name to my branch and made the necessary modifications to conclude AFAP.

theorem BHNeumann :
    (1 : ℚ) ≤ s.sum (fun i ↦ (1 : ℚ) / (H i).index) := sorry

#print axioms BHNeumann
'BHNeumann' depends on axioms: [propext, Quot.sound, Classical.choice]

It remains to deduce the conclusion about the number of cosets (it is immediate).

[Richard Copley]

(deleted)

[Richard Copley]

False alarm. I mixed up my s (the set of subgroups) with your s (the index set for the family of cosets).

[Antoine Chambert-Loir]

No worry.

[Richard Copley]

Antoine Chambert-Loir said:

It remains to deduce the conclusion about the number of cosets (it is immediate).

Done. (Easy, but can you make it look easy?)

[Antoine Chambert-Loir]

(I'll try, but this pigeonhole stuff is never so easy fo formalize, and one needs to cast back from Rat…)