FormalConjectures/ErdosProblems/1121.lean
Explanation legend Lean4 Domain Explanation Language (L4DEL)
L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.
- L4DEL
- Lean4 Domain Explanation Language
Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.
Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1
2 declarations, 2 contain sorry, 0 declared as axioms
Erdős Problem 1121
References:
- erdosproblems.com/1121
- [BeLi16] Bezdek, Károly and Litvak, Alexander E., Packing convex bodies by cylinders. Discrete Comput. Geom. (2016), 725-738.
- [GoGo45] Goodman, A. W. and Goodman, R. E., A circle covering theorem. Amer. Math. Monthly (1945), 494-498.
- [Ha47] Hadwiger, H., Nonseparable convex systems. Amer. Math. Monthly (1947), 583-585.
Imports (1)
- theorem
Erdos1121.erdos_1121Documented declaration: erdos_1121 sorry line 49 sourceSource documentation
If $C_1,\ldots,C_n$ are circles in $\mathbb{R}^2$ with radii $r_1,\ldots,r_n$ such that no line disjoint from all the circles divides them into two non-empty sets then the circles can be covered by a circle of radius $r=\sum r_i$.
This is true, and was proved by Goodman and Goodman [GoGo45] (whose proof also generalises to higher dimensions). A generalisation to convex bodies was proved by Hadwiger [Ha47].
An alternative proof is given by Bezdek and Litvak [BeLi16].
depends on sorry what this means
Statement uses:
Nat,Fin,EuclideanSpace,Real,OfNat.ofNat,LT.lt,Ne,ENNReal,Membership.mem,Set,Metric.closedBall,Inner.inner,Or,Exists,LE.le,Set.iUnion,Finset.sum,Finset.univProof uses:
sorryAx,Lean.Name,Bool.false,Lean.Name.num,Lean.Name.str,Lean.Name.anonymous66 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem erdos_1121 {n : ℕ} (c : Fin n → ℝ²) (r : Fin n → ℝ) (hr : ∀ i, 0 < r i) (hsep : ∀ (v : ℝ²) (t : ℝ), v ≠ 0 → (∀ i, ∀ p ∈ Metric.closedBall (c i) (r i), inner ℝ v p ≠ t) → (∀ i, inner ℝ v (c i) < t) ∨ (∀ i, t < inner ℝ v (c i))) : ∃ z : ℝ², (⋃ i, Metric.closedBall (c i) (r i)) ⊆ Metric.closedBall z (∑ i, r i) := by …Mentions: c
- theorem
Erdos1121.erdos_1121.variants.higher_dimensionDocumented declaration: higher_dimension sorry line 63 sourceSource documentation
The proof of Goodman and Goodman [GoGo45] also generalises to higher dimensions: if $B_1,\ldots,B_n$ are balls in $\mathbb{R}^d$ with radii $r_1,\ldots,r_n$ such that no hyperplane disjoint from all the balls divides them into two non-empty sets then the balls can be covered by a ball of radius $r=\sum r_i$.
depends on sorry what this means
Statement uses:
Nat,Fin,EuclideanSpace,Real,LT.lt,OfNat.ofNat,Ne,ENNReal,Membership.mem,Set,Metric.closedBall,Inner.inner,Or,Exists,LE.le,Set.iUnion,Finset.sum,Finset.univProof uses:
sorryAx,Lean.Name,Bool.false,Lean.Name.num,Lean.Name.str,Lean.Name.anonymous66 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem erdos_1121.variants.higher_dimension {d n : ℕ} (c : Fin n → EuclideanSpace ℝ (Fin d)) (r : Fin n → ℝ) (hr : ∀ i, 0 < r i) (hsep : ∀ (v : EuclideanSpace ℝ (Fin d)) (t : ℝ), v ≠ 0 → (∀ i, ∀ p ∈ Metric.closedBall (c i) (r i), inner ℝ v p ≠ t) → (∀ i, inner ℝ v (c i) < t) ∨ (∀ i, t < inner ℝ v (c i))) : ∃ z : EuclideanSpace ℝ (Fin d), (⋃ i, Metric.closedBall (c i) (r i)) ⊆ Metric.closedBall z (∑ i, r i) := by …Mentions: c