1Axiom Prover (Axiom Math)207 solved
Problems uniquely solved by this model
Pannwitz–Kuperberg quadrisecant theorem
smooth_knot_has_quadrisecant
#1
Verso theorem preview
theorem declaration uses `sorry`smooth_knot_has_quadrisecant {r : ℝ → LeanEval.KnotTheory.Quadrisecant.Space} (_hknot : LeanEval.KnotTheory.Quadrisecant.IsSmoothKnot r) (_hnontrivial : ¬ LeanEval.KnotTheory.Quadrisecant.IsUnknotted r) :
LeanEval.KnotTheory.Quadrisecant.HasQuadrisecant r := r:ℝ → Space_hknot:IsSmoothKnot r_hnontrivial:¬IsUnknotted r⊢ HasQuadrisecant r
All goals completed! 🐙
Bounded gaps between primes
zhang_bounded_prime_gaps
#2
Verso theorem preview
theorem declaration uses `sorry`zhang_bounded_prime_gaps :
∀ n : ℕ, ∃ p q : ℕ, n ≤ p ∧ p.Prime ∧ q.Prime ∧ p < q ∧ q - p ≤ 246 := ⊢ ∀ (n : ℕ), ∃ p q, n ≤ p ∧ Nat.Prime p ∧ Nat.Prime q ∧ p < q ∧ q - p ≤ 246
All goals completed! 🐙
Inscribed rectangles in a smooth Jordan curve attain at least one third of all aspect ratios
annals_inscribed_rectangles
#3
Verso theorem preview
theorem declaration uses `sorry`theorem_1 (γ : Circle → ℝ × ℝ) (hγ : IsSmoothEmbedding (𝓡 1) 𝓘(ℝ, ℝ × ℝ) ∞ γ) :
volume (X γ) ≥ 1/3 := γ:Circle → ℝ × ℝhγ:IsSmoothEmbedding (𝓡 1) 𝓘(ℝ, ℝ × ℝ) ∞ γ⊢ volume (X γ) ≥ 1 / 3
All goals completed! 🐙Other solved problems
Quantifier elimination for the theory of real closed fields
rcf_quantifier_elimination
#4
Verso theorem preview
/--
Quantifier elimination: `qe φ` is a quantifier-free formula equivalent to `φ` over `ℝ` in
every environment. Its syntax may mention additional variables vacuously.
-/
def declaration uses `sorry`qe (φ : Formula) : Formula := sorry/-- The output of `qe` is quantifier free. -/
theorem declaration uses `sorry`isQF_qe (φ : Formula) : (qe φ).IsQF := sorry/-- The output of `qe` is equivalent to its input, under every environment. -/
theorem declaration uses `sorry`holds_qe (φ : Formula) (env : Nat → ℝ) :
(qe φ).Holds env ↔ φ.Holds env := sorry/--
Anti-vacuity guard for the semantics and de Bruijn convention: a real number is a square
exactly when it is nonnegative.
-/
theorem declaration uses `sorry`holds_ex_sq (env : Nat → ℝ) :
(Formula.ex (.eq (.mul (.var 0) (.var 0)) (.var 1))).Holds env ↔
(Formula.not (.lt (.var 0) (.const 0))).Holds env := sorry
Topological classification of surfaces
topological_classification_of_surfaces
#5
Verso theorem preview
theorem declaration uses `sorry`classification_of_surfaces (S : Type*) [TopologicalSpace S]
[T2Space S] [ConnectedSpace S] [CompactSpace S]
[ChartedSpace (EuclideanHalfSpace 2) S]
[IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] :
Nonempty (S ≃ₜ Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1) ∨
∃ p n, ((1 ≤ p ∨ 1 ≤ n) ∧ Nonempty (S ≃ₜ Quot (LeanEval.Topology.ClassificationOfSurfaces.OrientableRel p n))) ∨
(1 ≤ p ∧ Nonempty (S ≃ₜ Quot (LeanEval.Topology.ClassificationOfSurfaces.NonOrientableRel p n))) := S:Type u_1inst✝⁵:TopologicalSpace Sinst✝⁴:T2Space Sinst✝³:ConnectedSpace Sinst✝²:CompactSpace Sinst✝¹:ChartedSpace (EuclideanHalfSpace 2) Sinst✝:IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S⊢ Nonempty (S ≃ₜ ↑(Metric.sphere 0 1)) ∨
∃ p n,
(1 ≤ p ∨ 1 ≤ n) ∧ Nonempty (S ≃ₜ Quot (OrientableRel p n)) ∨ 1 ≤ p ∧ Nonempty (S ≃ₜ Quot (NonOrientableRel p n))
All goals completed! 🐙
Pseudorandom sets in Grassmann graph have near-perfect expansion
annals_pseudorandom_grassmann
#6
Verso theorem preview
theorem declaration uses `sorry`theorem_1_12 (α : ℝ) (hα : α ∈ Set.Ioo 0 1) :
∃ ε > 0, ∃ r, ∀ᶠ (ℓ : ℕ) (k : ℕ) in atTop, ∀ S : Finset (PseudorandomGrassmann.GrVertex k ℓ),
(hS : S.Nonempty) → 2 * #S ≤ Fintype.card (PseudorandomGrassmann.GrVertex k ℓ) →
Φ (PseudorandomGrassmann.Gr k ℓ) S hS ≤ α → ∃ (A B : Submodule 𝔽₂ (Fin k → 𝔽₂)), A ≤ B ∧
letI a := finrank 𝔽₂ A; letI b := k - finrank 𝔽₂ B
a + b ≤ r ∧ #(S ∩ SubGr k ℓ A B) / #(SubGr k ℓ A B) ≥ (ε : ℝ) := α:ℝhα:α ∈ Set.Ioo 0 1⊢ ∃ ε > 0,
∃ r,
∀ᶠ (ℓ : ℕ) (k : ℕ) in atTop,
∀ (S : Finset (GrVertex k ℓ)) (hS : S.Nonempty),
2 * #S ≤ Fintype.card (GrVertex k ℓ) →
↑(Φ (Gr k ℓ) S hS) ≤ α →
∃ A B, A ≤ B ∧ finrank 𝔽₂ ↥A + (k - finrank 𝔽₂ ↥B) ≤ r ∧ ↑(#(S ∩ SubGr k ℓ A B)) / ↑(#(SubGr k ℓ A B)) ≥ ε
All goals completed! 🐙
Mihăilescu's theorem
mihailescu
#7
Verso theorem preview
theorem declaration uses `sorry`mihailescu {x y m n : ℕ}
(hx : 0 < x) (hy : 0 < y) (hm : 1 < m) (hn : 1 < n)
(h : x ^ m = y ^ n + 1) :
x = 3 ∧ y = 2 ∧ m = 2 ∧ n = 3 := x:ℕy:ℕm:ℕn:ℕhx:0 < xhy:0 < yhm:1 < mhn:1 < nh:x ^ m = y ^ n + 1⊢ x = 3 ∧ y = 2 ∧ m = 2 ∧ n = 3
All goals completed! 🐙
Enumerating number fields
annals_enumerating_number_fields
#8
Verso theorem preview
/--
Statement of Theorem 1 (Number fields have small models):
There exists a positive constant `Q` such that the following is true. Let `K` be a number field
of degree `n ≥ Q` and root discriminant `δ` over `ℚ`. Then there exist integers `r ≤ Q log n` and
`d ≤ Q log n` such that `(d + r) choose r ≤ Q n log n`, and there exist `r` polynomials
`E₁, ..., Eᵣ` of degree `≤ d` in `ℤ[x₁, ..., xᵣ]` all having coefficients bounded in absolute value
by `(n δ) ^ (Q log n)` such that the (smooth and zero-dimensional affine) scheme with equations
`E₁ = ... = Eᵣ = 0` and `det (∂Eᵢ/∂xⱼ) ≠ 0` contains `Spec K` as one of its irreducible components.
-/
theorem declaration uses `sorry`theorem_1 : ∃ Q > 0, ∀ n ≥ Q, ∀ K : NumberFieldOfDegree n, ∃ (r d : ℕ),
r ≤ Q * log n ∧ d ≤ Q * log n ∧ (d + r).choose r ≤ Q * n * log n ∧
∃ E : Fin r → MvPolynomial (Fin r) ℤ, (∀ i, (E i).totalDegree ≤ d) ∧
(∀ i j, |(E i).coeff j| ≤ (n * rootDiscr K) ^ (Q * log n)) ∧
letI X := nonsingularOpen fun i ↦ (E i).map (algebraMap ℤ ℚ)
∃ Z, ∃ hZ : Z ∈ irreducibleComponents X,
Nonempty (X.irreducibleComponent Z hZ ≅ Spec (.of K)) := ⊢ ∃ Q > 0,
∀ n ≥ Q,
∀ (K : NumberFieldOfDegree n),
∃ r d,
↑r ≤ ↑Q * log ↑n ∧
↑d ≤ ↑Q * log ↑n ∧
↑((d + r).choose r) ≤ ↑Q * ↑n * log ↑n ∧
∃ E,
(∀ (i : Fin r), (E i).totalDegree ≤ d) ∧
(∀ (i : Fin r) (j : Fin r →₀ ℕ),
↑|MvPolynomial.coeff j (E i)| ≤ (↑n * rootDiscr K.carrier) ^ (↑Q * log ↑n)) ∧
∃ Z,
∃ (hZ :
Z ∈
irreducibleComponents ↥(nonsingularOpen fun i => (MvPolynomial.map (algebraMap ℤ ℚ)) (E i))),
Nonempty
((nonsingularOpen fun i => (MvPolynomial.map (algebraMap ℤ ℚ)) (E i)).irreducibleComponent Z
hZ ≅
Spec (CommRingCat.of K.carrier))
All goals completed! 🐙/--
Statement of Theorem 2 (Number fields with bounded discriminant):
There exists a positive constant `Q` such that the following is true. Let `n ≥ Q` be an integer.
Let `H ≥ 1` be an integer. The number of isomorphism classes of number fields
with degree `n` and discriminant `≤ H` is `≤ n^(Q n log^3 n) H^(Q log^3 n)`.
-/
theorem declaration uses `sorry`theorem_2 : ∃ Q > 0, ∀ n ≥ Q, ∀ H ≥ 1,
(Nat.card (NumberFieldOfBoundedDiscriminantUpToIsomorphism n H) : ℝ) ≤
n ^ (Q * n * log n ^ 3) * H ^ (Q * log n ^ 3) := ⊢ ∃ Q > 0,
∀ n ≥ Q,
∀ H ≥ 1,
↑(Nat.card (NumberFieldOfBoundedDiscriminantUpToIsomorphism n H)) ≤
↑n ^ (↑Q * ↑n * log ↑n ^ 3) * ↑H ^ (↑Q * log ↑n ^ 3)
All goals completed! 🐙
Fractal uncertainty in higher dimensions
annals_fractal_uncertainty
#9
Verso theorem preview
theorem declaration uses `sorry`theorem_1_1 (ν : ℝ) (hν₀ : 0 < ν) :
∃ (β C : ℝ), β > 0 ∧ C > 0 ∧ ∀ (h : ℝ) (X Y : Set ℝᵈ)
(hX : MeasurableSet X) (hY : MeasurableSet Y), h ∈ Set.Ioo 0 (1 / 100) →
X ⊆ FractalUncertainty.cube (-1) 1 → FractalUncertainty.PorousOnBalls ν h 1 X → Y ⊆ FractalUncertainty.cube (-h⁻¹) h⁻¹ →
FractalUncertainty.PorousOnLines ν 1 h⁻¹ Y → ∀ (f : Lp ℂ 2), (𝓕 f : Lp ℂ 2) =ᵐ[volume.restrict Yᶜ] 0 →
(eLpNorm (X.indicator f) 2).toReal ≤ C * h ^ β * ‖f‖ := d:ℕν:ℝhν₀:0 < ν⊢ ∃ β C,
β > 0 ∧
C > 0 ∧
∀ (h : ℝ) (X Y : Set ℝᵈ),
MeasurableSet X →
MeasurableSet Y →
h ∈ Set.Ioo 0 (1 / 100) →
X ⊆ cube (-1) 1 →
PorousOnBalls ν h 1 X →
Y ⊆ cube (-h⁻¹) h⁻¹ →
PorousOnLines ν 1 h⁻¹ Y →
∀ (f : ↥(Lp ℂ 2 volume)),
↑↑(𝓕 f) =ᵐ[volume.restrict Yᶜ] 0 → (eLpNorm (X.indicator ↑↑f) 2 volume).toReal ≤ C * h ^ β * ‖f‖
All goals completed! 🐙
New large value estimates for Dirichlet polynomials
annals_large_value_estimates
#10
Verso theorem preview
theorem declaration uses `sorry`theorem_1_1 : ∃ o : ℝ → ℝ, o =o[Filter.atTop] (1 : ℝ → ℝ) ∧
∀ (b : ℕ → ℂ) (_hb : ∀ n, ‖b n‖ ≤ 1) (N : ℕ) (V : ℝ) (T : ℝ) (R : ℕ) (t : Fin R → ℝ),
N > 0 → V > 0 → T > 1 → -- these assumptions are necessary but not stated in the paper
(∀ i j, i ≠ j → |t i - t j| ≥ 1) → (∀ i, t i ∈ Set.Icc 0 T) →
(∀ r, ‖∑ n ∈ Finset.Icc N (2 * N), b n * n ^ (I * t r)‖ ≥ V) →
R ≤ T ^ (o T) * bound N V T := ⊢ ∃ o,
o =o[Filter.atTop] 1 ∧
∀ (b : ℕ → ℂ),
(∀ (n : ℕ), ‖b n‖ ≤ 1) →
∀ (N : ℕ) (V T : ℝ) (R : ℕ) (t : Fin R → ℝ),
N > 0 →
V > 0 →
T > 1 →
(∀ (i j : Fin R), i ≠ j → |t i - t j| ≥ 1) →
(∀ (i : Fin R), t i ∈ Set.Icc 0 T) →
(∀ (r : Fin R), ‖∑ n ∈ Finset.Icc N (2 * N), b n * ↑n ^ (I * ↑(t r))‖ ≥ V) →
↑R ≤ T ^ o T * bound N V T
All goals completed! 🐙
Topological sphere theorem (Berger–Klingenberg–Rauch)
sphere_theorem_topological
#11
Lean theorem statement
/-- **Topological sphere theorem** (Berger–Klingenberg–Rauch 1960). A closed,
simply-connected, smooth `d`-manifold (`d ≥ 2`) whose Levi-Civita connection is
strictly quarter-pinched is homeomorphic to the standard `d`-sphere. -/
theorem sphere_theorem
[I.Boundaryless] [T2Space M] [CompactSpace M] [SimplyConnectedSpace M]
(hdim : 2 ≤ Module.finrank ℝ E)
(cov : CovariantDerivative I E (TangentSpace I (M := M)))
[ContMDiffCovariantDerivative cov ∞]
(_htor : cov.torsion = 0) (_hmet : IsMetricCompatible cov)
(_hpinch : QuarterPinched cov) :
Nonempty
(M ≃ₜ sphere (0 : EuclideanSpace ℝ (Fin (Module.finrank ℝ E + 1))) 1) := by
sorry
Uniformization theorem for Riemann surfaces
uniformization
#12
Verso theorem preview
theorem declaration uses `sorry`uniformization {X : Type*} [TopologicalSpace X] [T2Space X] [ConnectedSpace X]
[SecondCountableTopology X] [ChartedSpace ℂ X] [IsManifold mℂ 1 X]
(hX : ¬ CompactSpace X) (x : X) [Subsingleton <| Additive (FundamentalGroup X x) →+ ℝ] :
Nonempty (X ≃ₘ⟮mℂ, mℂ⟯ ℂ) ∨ Nonempty (X ≃ₘ⟮mℂ, mℂ⟯ UpperHalfPlane) := X:Type u_1inst✝⁶:TopologicalSpace Xinst✝⁵:T2Space Xinst✝⁴:ConnectedSpace Xinst✝³:SecondCountableTopology Xinst✝²:ChartedSpace ℂ Xinst✝¹:IsManifold mℂ 1 XhX:¬CompactSpace Xx:Xinst✝:Subsingleton (Additive (FundamentalGroup X x) →+ ℝ)⊢ Nonempty (X ≃ₘ⟮mℂ, mℂ⟯ ℂ) ∨ Nonempty (X ≃ₘ⟮mℂ, mℂ⟯ UpperHalfPlane)
All goals completed! 🐙
A negative answer to Ulam's Problem 19 from the Scottish Book
annals_ulam
#13
Verso theorem preview
theorem declaration uses `sorry`theorem_1 (hd : 3 ≤ d) : letI : NeZero d := ⟨d:ℕhd:3 ≤ d⊢ d ≠ 0 All goals completed! 🐙⟩
∃ K : Ulam.BodyOfRevolution d, Ulam.IsStrictlyConvexBody K.body ∧ ¬ Ulam.IsCentrallySymmetric K.body ∧
Ulam.FloatsInEquilibriumInEveryOrientationAtLevel K.body (volume.real K.body / 2) := d:ℕhd:3 ≤ d⊢ ∃ K,
IsStrictlyConvexBody K.body ∧
¬IsCentrallySymmetric K.body ∧ FloatsInEquilibriumInEveryOrientationAtLevel K.body (volume.real K.body / 2)
All goals completed! 🐙
On Zagier-Hoffman's conjectures in positive characteristic
annals_zagier_hoffman_positive_char
#14
Verso theorem preview
/--
Statement of Theorem A (Brown's theorem in positive characteristic):
Let `w ∈ ℕ`, where `ℕ := {1,2,...}`. Then every MZV of weight `w` can be written as a `K`-linear
combination of MZV's in the set `𝒯_w`. In particular, `dim 𝒵_w ≤ d(w)`.
Note that `K` in the paper is `RatFunc F`.
-/
theorem declaration uses `sorry`theorem_A (w : ℕ+) :
𝒵 F w = Submodule.span (RatFunc F) (𝒯 F w) ∧
Module.rank (RatFunc F) (𝒵 F w) ≤ d F w := F:Type u_1inst✝²:Field Finst✝¹:Finite Finst✝:DecidableEq F⟮X⟯w:ℕ+⊢ 𝒵 F ↑w = Submodule.span F⟮X⟯ (𝒯 F ↑w) ∧ Module.rank F⟮X⟯ ↥(𝒵 F ↑w) ≤ ↑(d F ↑w)
All goals completed! 🐙/--
Statement of Theorem B:
Let `w ∈ ℕ`, where `ℕ := {1,2,...}`. MZVs of weight `w` in `𝒯0 w` are all linearly independent over
`K`. In particular, `dim 𝒵 w ≥ |𝒯0 w|`. Note that `K` in the paper is `RatFunc F`.
-/
theorem declaration uses `sorry`theorem_B (w : ℕ+) :
LinearIndependent (RatFunc F) (Subtype.val : 𝒯0 F w → CompletionAtInfty F) ∧
Module.rank (RatFunc F) (𝒵 F w) ≥ Set.ncard (𝒯0 F w) := F:Type u_1inst✝²:Field Finst✝¹:Finite Finst✝:DecidableEq F⟮X⟯w:ℕ+⊢ LinearIndependent F⟮X⟯ Subtype.val ∧ Module.rank F⟮X⟯ ↥(𝒵 F ↑w) ≥ ↑(𝒯0 F ↑w).ncard
All goals completed! 🐙/--
Statement of Theorem D:
Let `w ∈ ℕ+` with `w ≤ 2q − 2`. Then `𝒯 w` is a `K`-basis for `𝒵 w`. In particular,
`dim_K (𝒵 w) = d(w)`. Note that `K` in the paper is `RatFunc F`.
Note: Theorem A establishes that `𝒯 w` spans `𝒵 w`. So to prove `𝒯 w` is a `K`-basis for `𝒵 w`, we
only need to show that `𝒯 w` are linearly independent in `𝒵 w`.
-/
theorem declaration uses `sorry`theorem_D (w : ℕ+) (hw : w ≤ 2 * Nat.card F - 2) :
LinearIndependent (RatFunc F) (Subtype.val : 𝒯 F w → CompletionAtInfty F) ∧
Module.rank (RatFunc F) (𝒵 F w) = d F w := F:Type u_1inst✝²:Field Finst✝¹:Finite Finst✝:DecidableEq F⟮X⟯w:ℕ+hw:↑w ≤ 2 * Nat.card F - 2⊢ LinearIndependent F⟮X⟯ Subtype.val ∧ Module.rank F⟮X⟯ ↥(𝒵 F ↑w) = ↑(d F ↑w)
All goals completed! 🐙
Erdős's unit-distance conjecture is false
erdos_unit_distance_conjecture_false
#15
Verso theorem preview
theorem declaration uses `sorry`erdos_unit_distance_conjecture_false :
∃ δ : ℝ, 0 < δ ∧
∀ N : ℕ, ∃ (n : ℕ) (P : Finset (EuclideanSpace ℝ (Fin 2))),
N ≤ n ∧ P.card = n ∧ (n : ℝ) ^ (1 + δ) ≤ (unitDist P : ℝ) := ⊢ ∃ δ, 0 < δ ∧ ∀ (N : ℕ), ∃ n P, N ≤ n ∧ P.card = n ∧ ↑n ^ (1 + δ) ≤ ↑(unitDist P)
All goals completed! 🐙
Flat Littlewood polynomials exist
annals_flat_littlewood_poly
#16
Lean theorem statement
/--
Statement of Theorem 1.1:
There exist constants `∆ > δ > 0` such that, for all `n ≥ 2`, there exists a Littlewood
polynomial `P(z)` of degree `n` with `δ√n ≤ |P (z)| ≤ ∆√n` for all `z ∈ ℂ` with `|z| = 1`.
-/
theorem theorem_1_1 :
∃ Δ δ : ℝ, Δ > δ ∧ δ > 0 ∧ ∀ n ≥ 2,
∃ P : ℂ[X], IsLittlewoodPolynomial P ∧ P.natDegree = n ∧
∀ z : ℂ, ‖z‖ = 1 → δ * √n ≤ ‖P.eval z‖ ∧
‖P.eval z‖ ≤ Δ * √n := by
sorry
Lorentzian polynomials
annals_lorentzian_polynomials
#17
Verso theorem preview
theorem declaration uses `sorry`theorem_2_25 (n d : ℕ) (hn : 0 < n) : closure (Ŀ n d) = LorentzianPolynomials.L n d := n:ℕd:ℕhn:0 < n⊢ closure (Ŀ n d) = L n d
All goals completed! 🐙
Galois groups of random integer polynomials and van der Waerden's Conjecture
annals_van_der_waerden_conjecture
#18
Verso theorem preview
theorem declaration uses `sorry`theorem_1 (n : ℕ) (hn : 3 ≤ n) :
(fun H ↦ (vanDerWaerdenConjecture.E n H : ℝ)) =O[atTop] (fun H ↦ (H ^ (n - 1) : ℝ)) := n:ℕhn:3 ≤ n⊢ (fun H => ↑(E n H)) =O[atTop] fun H => ↑H ^ (n - 1)
All goals completed! 🐙
A counterexample to the periodic tiling conjecture
annals_periodic_tiling_conjecture
#19
Verso theorem preview
/--
Statement of Theorem 1.4 (Counterexample to Conjecture 1.2, I):
There exists a finite abelian group `G₀` and a finite non-empty `F ⊆ ℤ² × G₀` such that
`F` forms an aperiodic tiling equation.
-/
theorem declaration uses `sorry`theorem_1_4 : ∃ (G₀ : Type) (_ : AddCommGroup G₀) (_ : Finite G₀),
∃ F : Set (ℤ × ℤ × G₀), F.Finite ∧ F.Nonempty ∧ IsAperiodicTilingEquation F := ⊢ ∃ G₀ x, ∃ (_ : Finite G₀), ∃ F, F.Finite ∧ F.Nonempty ∧ IsAperiodicTilingEquation F
All goals completed! 🐙/--
Statement of Corollary 1.6 (Counterexample to Conjecture 1.2, II):
For all sufficiently large `d`, there exists a finite non-empty `F ⊆ ℤᵈ` such that
`F` forms an aperiodic tiling equation.
-/
theorem declaration uses `sorry`corollary_1_6 : ∀ᶠ d in atTop, ∃ (F : Set (Fin d → ℤ)),
F.Finite ∧ F.Nonempty ∧ IsAperiodicTilingEquation F := ⊢ ∀ᶠ (d : ℕ) in atTop, ∃ F, F.Finite ∧ F.Nonempty ∧ IsAperiodicTilingEquation F
All goals completed! 🐙/--
Statement of Corollary 1.7 (Counterexample to Conjecture 1.3):
For all sufficiently large `d`, there exists a bounded measurable set `σ ⊆ ℝᵈ` of positive
measure such that `σ` forms an aperiodic continuous tiling equation.
-/
theorem declaration uses `sorry`corollary_1_7 : ∀ᶠ d in atTop, ∃ σ : Set (Fin d → ℝ), IsBounded σ ∧ MeasurableSet σ ∧
0 < volume σ ∧ IsAperiodicContinuousTilingEquation σ := ⊢ ∀ᶠ (d : ℕ) in atTop, ∃ σ, Bornology.IsBounded σ ∧ MeasurableSet σ ∧ 0 < volume σ ∧ IsAperiodicContinuousTilingEquation σ
All goals completed! 🐙
On a conjecture of Marton
annals_conjecture_of_marton
#20
Verso theorem preview
theorem declaration uses `sorry`theorem_1_2 (A : Set (ConjectureOfMarton.F n)) (K : ℝ) (h₀ : A.Nonempty) (h : (A + A).ncard ≤ K * A.ncard) :
∃ H : AddSubgroup (ConjectureOfMarton.F n), Nat.card H ≤ A.ncard ∧ CovByVAdd (ConjectureOfMarton.F n) (2 * K ^ 12) A H := n:ℕA:Set (F n)K:ℝh₀:A.Nonemptyh:↑(A + A).ncard ≤ K * ↑A.ncard⊢ ∃ H, Nat.card ↥H ≤ A.ncard ∧ CovByVAdd (F n) (2 * K ^ 12) A ↑H
All goals completed! 🐙
De Branges's theorem (Bieberbach conjecture)
deBranges_theorem
#21
Verso theorem preview
theorem declaration uses `sorry`deBranges (f : ℂ → ℂ) (diff : DifferentiableOn ℂ f (ball 0 1)) (inj : (ball 0 1).InjOn f)
(h0 : f 0 = 0) (h1 : deriv f 0 = 1) (n : ℕ) : ‖iteratedDeriv n f 0 / n.factorial‖ ≤ n := f:ℂ → ℂdiff:DifferentiableOn ℂ f (ball 0 1)inj:Set.InjOn f (ball 0 1)h0:f 0 = 0h1:deriv f 0 = 1n:ℕ⊢ ‖iteratedDeriv n f 0 / ↑n.factorial‖ ≤ ↑n
All goals completed! 🐙
On a conjecture of Talagrand on selector processes and a consequence on positive empirical processes
annals_supremum_of_selector_processes
#22
Verso theorem preview
/-- The constant `L` of Theorem 1.2. -/
noncomputable def declaration uses `sorry`L₂ : ℝ≥0 := sorry/-- The constant of Theorem 1.2 is positive. -/
theorem declaration uses `sorry`L₂_pos : L₂ > 0 := sorry/--
Statement of Theorem 1.2:
There exists `L > 0` such that for any `0 < p < 1`, finite type `X`, and set `Λ` of functions from
`X` to `ℝ≥0` such that `0 < 𝔼[sup_{f ∈ Λ} ∑ i ∈ Xp, f i] < ∞`, the collection of sets
`{s ⊆ X | sup_{f ∈ Λ} ∑ i ∈ s, f i ≥ L * 𝔼[sup_{f ∈ Λ} ∑ i ∈ Xp, f i]}`
is `p-small`, where `Xp` is a binomial random subset of `X` with parameter `p`.
Note: The assumption `0 < 𝔼[sup_{f ∈ Λ} ∑ i ∈ Xp, f i] < ∞` is not explicitly stated in the theorem
but used in the last step of the proof where `𝔼 ≥ (L/L') * 𝔼` is a contradiction for `L > L'`.
-/
theorem declaration uses `sorry`theorem_1_2 (p : I) (hp₀ : 0 < p) (hp₁ : p < 1) (X : Type*) [Fintype X] (Λ : Set (X → ℝ≥0))
(hE₀ : 0 < 𝔼⁻[⨆ f ∈ Λ, ∑ i ∈ Xp, (f i : ℝ≥0∞); Xp ∼ binomialSetDistribution X p])
(hE : 𝔼⁻[⨆ f ∈ Λ, ∑ i ∈ Xp, (f i : ℝ≥0∞); Xp ∼ binomialSetDistribution X p] < ∞) :
IsSmall p {s : Set X | ⨆ f ∈ Λ, ∑ i ∈ s, (f i : ℝ≥0∞) ≥
L₂ * 𝔼⁻[⨆ f ∈ Λ, ∑ i ∈ Xp, (f i : ℝ≥0∞); Xp ∼ binomialSetDistribution X p]} := p:↑Ihp₀:0 < php₁:p < 1X:Type u_1inst✝:Fintype XΛ:Set (X → ℝ≥0)hE₀:0 < ∫⁻ (Xp : Set X), ⨆ f ∈ Λ, ∑ i ∈ Xp.toFinset, ↑(f i) ∂binomialSetDistribution X phE:∫⁻ (Xp : Set X), ⨆ f ∈ Λ, ∑ i ∈ Xp.toFinset, ↑(f i) ∂binomialSetDistribution X p < ∞⊢ IsSmall p
{s |
⨆ f ∈ Λ, ∑ i ∈ s.toFinset, ↑(f i) ≥
↑L₂ * ∫⁻ (Xp : Set X), ⨆ f ∈ Λ, ∑ i ∈ Xp.toFinset, ↑(f i) ∂binomialSetDistribution X p}
All goals completed! 🐙/-- The constant `L` of Theorem 1.3. -/
noncomputable def declaration uses `sorry`L₃ : ℝ≥0 := sorry/-- The constant of Theorem 1.3 is positive. -/
theorem declaration uses `sorry`L₃_pos : L₃ > 0 := sorry/--
Statement of Theorem 1.3:
There exists `L > 0` such that for any `N > 0`, i.i.d random variables `Y_1, …, Y_N` distributed
according to a Borel probability measure `ν` on a Polish space `𝕋`, if `𝓕` is a finite set of
non-negative functions in `L∞(𝕋)` and `0 < 𝔼[sup_{f ∈ 𝓕} Z Y f] < ∞` then there exists a finite
collection `𝓒` of pairs `(g, t)` where `g : 𝕋 → ℝ≥0`, `t > 0` such that
`{sup_{f ∈ 𝓕} Z N Y f ≥ L * 𝔼[sup_{f ∈ 𝓕} Z N Y f] } ⊆ ⋃ (g,t) ∈ 𝓒, {t ≤ Z N Y g}`
and
`∑ (g,t) ∈ 𝓒, P(t ≤ Z N Y g) ≤ 2⁻¹`.
Note: The requirement that the collection `𝓒` be finite is not explicitly stated in the paper.
However, `𝓒` must at least be assumed to be countable in order for the sum to make sense,
and the collections `𝓒` produced by the proof are indeed finite.
-/
theorem declaration uses `sorry`theorem_1_3 (N : ℕ) (N_pos : N > 0) (𝕋 : Type*) (t𝕋 : TopologicalSpace 𝕋)
(p𝕋 : PolishSpace 𝕋)
(m𝕋 : MeasurableSpace 𝕋) (b𝕋 : BorelSpace 𝕋) (ν : Measure 𝕋) (hν : IsProbabilityMeasure ν)
(Ω : Type*) (mΩ : MeasurableSpace Ω) (P : Measure Ω) (Y : Fin N → Ω → 𝕋)
(Y_indep : iIndepFun Y P) (Y_law_ν : ∀ i, HasLaw (Y i) ν P)
(𝓕 : Set {f : 𝕋 → ℝ≥0 // Measurable f ∧ MemLp f ∞ ν}) (h𝓕 : Finite 𝓕)
(hZ₀ : 0 < 𝔼⁻[⨆ f ∈ 𝓕, (Z N Y f ·); P]) (hZ : 𝔼⁻[⨆ f ∈ 𝓕, (Z N Y f ·); P] < ∞) :
∃ 𝓒 : Finset ({g : 𝕋 → ℝ≥0 // Measurable g} × {t : ℝ≥0 | t > 0}),
{ω | ⨆ f ∈ 𝓕, Z N Y f ω ≥ L₃ * 𝔼⁻[⨆ f ∈ 𝓕, (Z N Y f ·); P]} ⊆ ⋃ c ∈ 𝓒, {ω | c.2 ≤ Z N Y c.1 ω}
∧ ∑ c : 𝓒, P {ω | c.val.2 ≤ Z N Y c.val.1 ω} ≤ 2⁻¹ := N:ℕN_pos:N > 0𝕋:Type u_1t𝕋:TopologicalSpace 𝕋p𝕋:PolishSpace 𝕋m𝕋:MeasurableSpace 𝕋b𝕋:BorelSpace 𝕋ν:Measure 𝕋hν:IsProbabilityMeasure νΩ:Type u_2mΩ:MeasurableSpace ΩP:Measure ΩY:Fin N → Ω → 𝕋Y_indep:iIndepFun Y PY_law_ν:∀ (i : Fin N), HasLaw (Y i) ν P𝓕:Set { f // Measurable f ∧ MemLp f ∞ ν }h𝓕:Finite ↑𝓕hZ₀:0 < ∫⁻ (ω : Ω), ↑((⨆ f ∈ 𝓕, fun x => Z N Y (↑f) x) ω) ∂PhZ:∫⁻ (ω : Ω), ↑((⨆ f ∈ 𝓕, fun x => Z N Y (↑f) x) ω) ∂P < ∞⊢ ∃ 𝓒,
{ω | ↑(⨆ f ∈ 𝓕, Z N Y (↑f) ω) ≥ ↑L₃ * ∫⁻ (ω : Ω), ↑((⨆ f ∈ 𝓕, fun x => Z N Y (↑f) x) ω) ∂P} ⊆
⋃ c ∈ 𝓒, {ω | ↑c.2 ≤ Z N Y (↑c.1) ω} ∧
∑ c, P {ω | ↑(↑c).2 ≤ Z N Y (↑(↑c).1) ω} ≤ 2⁻¹
All goals completed! 🐙
Green–Tao theorem
green_tao
#23
Verso theorem preview
theorem declaration uses `sorry`green_tao : LeanEval.NumberTheory.ContainsArbitraryAPs {p : ℕ | Nat.Prime p} := ⊢ ContainsArbitraryAPs {p | Nat.Prime p}
All goals completed! 🐙
Morley's categoricity theorem
morley_categoricity_theorem
#24
Verso theorem preview
theorem declaration uses `sorry`morley_categoricity_theorem (L : FirstOrder.Language.{0, 0}) (hL : L.card ≤ ℵ₀)
(T : L.Theory) (hT : T.IsComplete)
(hInf : ∀ M : FirstOrder.Language.Theory.ModelType.{0, 0, 0} T, Infinite M)
{κ : Cardinal.{0}} (hκ : ℵ₀ < κ) (hcat : κ.Categorical T)
{μ : Cardinal.{0}} (hμ : ℵ₀ < μ) :
μ.Categorical T := L:FirstOrder.LanguagehL:L.card ≤ ℵ₀T:L.TheoryhT:T.IsCompletehInf:∀ (M : T.ModelType), Infinite ↑Mκ:Cardinal.{0}hκ:ℵ₀ < κhcat:κ.Categorical Tμ:Cardinal.{0}hμ:ℵ₀ < μ⊢ μ.Categorical T
All goals completed! 🐙
Improved bounds for the sunflower lemma
annals_improved_bounds_sunflower_lemma
#25
Verso theorem preview
/-- The absolute constant `C` in Theorem 1.4. Although not explicitly stated in the paper,
the constant `C` doesn't depend on `r`. -/
noncomputable def declaration uses `sorry`C : ℝ := sorry/--
Statement of Theorem 1.4 (Main theorem, sunflowers):
Let `r ≥ 3`. For some constant `C`, any `w`-set system `F` of size
`|F| ≥ (C * r ^ 3 * log w * log log w) ^ w` contains an `r`-sunflower.
Note: We require `w ≥ 2`, as the paper assumes `log log w > 0`.
-/
theorem declaration uses `sorry`theorem_1_4 (r : ℕ) (hr : r ≥ 3) (X : Type*) [Finite X] (ℱ : Set (Set X)) (w : ℕ)
(hw : w ≥ 2) (hℱ₁ : ℱ.IsSystem w) (hℱ₂ : ℱ.ncard ≥ lowerBound r C w) :
∃ S ⊆ ℱ, S.IsSunflower r := r:ℕhr:r ≥ 3X:Type u_1inst✝:Finite Xℱ:Set (Set X)w:ℕhw:w ≥ 2hℱ₁:Set.IsSystem w ℱhℱ₂:↑ℱ.ncard ≥ lowerBound r C w⊢ ∃ S ⊆ ℱ, Set.IsSunflower r S
All goals completed! 🐙
On approximation to a real number by algebraic numbers of bounded degree
annals_on_approximation_of_reals
#26
Verso theorem preview
theorem declaration uses `sorry`theorem_1_1 (n : ℕ) (hn : n ≥ 2) (ξ : ℝ) (hξ : Transcendental ℚ ξ) :
letI a : ℝ := 1 / (2 - Real.log 2)
(ω⋆ n ξ : EReal) ≥ (a : EReal) * n := n:ℕhn:n ≥ 2ξ:ℝhξ:Transcendental ℚ ξ⊢ ↑(ω⋆ n ξ) ≥ ↑(1 / (2 - Real.log 2)) * ↑n
All goals completed! 🐙
Viscosity solutions and hyperbolic motions: a new PDE method for the N-body problem
annals_viscosity_solutions
#27
Verso theorem preview
theorem declaration uses `sorry`theorem_1_1 (hE : 2 ≤ Module.finrank ℝ E) (m : ℝᴺ) (hm : ∀ i, 0 < m i)
(x₀ a : Eᴺ) (a_nc : ViscositySolutions.WithoutCollisions a) (a_norm : ‖a‖_[m] = 1) (h : ℝ) (h_pos : h > 0) :
∃ x : ℝ → Eᴺ, ∃ o : ℝ → Eᴺ, (o =o[atTop] fun t ↦ t) ∧ x 0 = x₀ ∧
ViscositySolutions.IsNBodySolution m x ∧ (∀ t > 0, ViscositySolutions.WithoutCollisions (x t)) ∧
∀ t ≥ 0, x t = (sqrt (2 * h) * t) • a + o t := E:Type u_1inst✝²:NormedAddCommGroup Einst✝¹:InnerProductSpace ℝ Einst✝:FiniteDimensional ℝ EN:ℕhE:2 ≤ Module.finrank ℝ Em:Fin N → ℝhm:∀ (i : Fin N), 0 < m ix₀:Eᴺa:Eᴺa_nc:WithoutCollisions aa_norm:‖a‖_[m] = 1h:ℝh_pos:h > 0⊢ ∃ x o,
(o =o[atTop] fun t => t) ∧
x 0 = x₀ ∧ IsNBodySolution m x ∧ (∀ t > 0, WithoutCollisions (x t)) ∧ ∀ t ≥ 0, x t = (√(2 * h) * t) • a + o t
All goals completed! 🐙
Dimitrov's lower bound for the house of a nonzero algebraic integer that is not a root of unity
dimitrov
#28
Verso theorem preview
theorem declaration uses `sorry`dimitrov {K : Type*} [Field K] [NumberField K]
(α : K)
(α_int : IsIntegral ℤ α)
(α_ne_zero : α ≠ 0)
(α_not_rootOfUnity : ¬ IsOfFinOrder α) :
(2 : ℝ) ^ (1 / (4 * (Finset.univ.image fun σ : K →+* ℂ ↦ (σ α).arg).card) : ℝ) ≤
NumberField.house α := K:Type u_1inst✝¹:Field Kinst✝:NumberField Kα:Kα_int:IsIntegral ℤ αα_ne_zero:α ≠ 0α_not_rootOfUnity:¬IsOfFinOrder α⊢ 2 ^ (1 / (4 * ↑(Finset.image (fun σ => (σ α).arg) Finset.univ).card)) ≤ NumberField.house α
All goals completed! 🐙
Isoperimetric inequality (n-dim, topological-frontier form)
isoperimetric_inequality
#29
Verso theorem preview
theorem declaration uses `sorry`isoperimetric (n : ℕ) (_hn : 2 ≤ n) (B : Set (LeanEval.Geometry.E n))
(_hB : MeasurableSet B) (_hBdd : Bornology.IsBounded B) :
(n : ℝ≥0∞) ^ n * (volume B) ^ (n - 1) * volume (closedBall (0 : LeanEval.Geometry.E n) 1)
≤ (μHE[n - 1] (frontier B)) ^ n := n:ℕ_hn:2 ≤ nB:Set (E n)_hB:MeasurableSet B_hBdd:Bornology.IsBounded B⊢ ↑n ^ n * volume B ^ (n - 1) * volume (closedBall 0 1) ≤ μHE[n - 1] (frontier B) ^ n
All goals completed! 🐙
Singularity of random Bernoulli matrices
annals_random_bernoulli_matrices
#30
Verso theorem preview
/--
Statement of Theorem A:
For every `p ∈ (0, 1/2]` and `ε > 0` there exists `N, C > 0` such that for any `n ≥ N` and any
`n × n` random matrix `B` with mutually independent `Bernoulli(p)` entries,
`P(σ_min (B + sIIᵀ) ≤ t/√n) ≤ (1 - p + ε)ⁿ + Ct` for all `s ∈ [-1,0]` and `t > 0`.
-/
theorem declaration uses `sorry`theorem_A {p : I} {ε : ℝ} (hp₀ : 0 < p) (hp₁ : (p : ℝ) ≤ 1 / 2) (hε : 0 < ε) :
∃ N > 0, ∃ C > 0, ∀ n ≥ N,
∀ (Ω : Type*) (_mΩ : MeasurableSpace Ω) (P : Measure Ω) (B : Ω → Matrix (Fin n) (Fin n) ℝ)
(_B_indep : iIndepFun (fun x : Fin n × Fin n ↦ (B · x.1 x.2)) P)
(_B_bernoulli : ∀ i j, HasLaw (B · i j) (bernoulliMeasure 1 0 p) P),
∀ s : ℝ, -1 ≤ s ∧ s ≤ 0 → ∀ t : ℝ, 0 < t →
P.real {ω : Ω | σ_min (B ω + of (fun _ _ ↦ s)) ≤ t / √n} ≤ (1 - p + ε) ^ n + C * t := p:↑Iε:ℝhp₀:0 < php₁:↑p ≤ 1 / 2hε:0 < ε⊢ ∃ N > 0,
∃ C > 0,
∀ n ≥ N,
∀ (Ω : Type u_1) (_mΩ : MeasurableSpace Ω) (P : Measure Ω) (B : Ω → Matrix (Fin n) (Fin n) ℝ),
iIndepFun (fun x x_1 => B x_1 x.1 x.2) P →
(∀ (i j : Fin n), HasLaw (fun x => B x i j) Ber(1, 0, p) P) →
∀ (s : ℝ),
-1 ≤ s ∧ s ≤ 0 →
∀ (t : ℝ), 0 < t → P.real {ω | σ_min (B ω + of fun x x_1 => s) ≤ t / √↑n} ≤ (1 - ↑p + ε) ^ n + C * t
All goals completed! 🐙/--
This (unnamed) corollary appears directly below Theorem A in the paper:
For every `p ∈ (0, 1/2]` and any sequence `Bₙ` of `n × n` random matrices with mutually
independent `Bernoulli(p)` entries we have that
`P(Bₙ is singular) = (1 - p + oₙ(1))ⁿ`.
-/
theorem declaration uses `sorry`corollary_1 {p : I} (hp₀ : 0 < p) (hp₁ : (p : ℝ) ≤ 1 / 2)
{Ω : ℕ → Type*} [mΩ : ∀ n, MeasurableSpace (Ω n)] {P : (n : ℕ) → Measure (Ω n)}
{B : (n : ℕ) → Ω n → Matrix (Fin n) (Fin n) ℝ}
(B_indep : ∀ n, iIndepFun (fun x : Fin n × Fin n ↦ (B n · x.1 x.2)) (P n))
(B_bernoulli : ∀ n i j, HasLaw (B n · i j) (bernoulliMeasure 1 0 p) (P n)) :
∃ o : ℕ → ℝ, o =o[atTop] (1 : ℕ → ℝ) ∧
∀ n > 0, (P n).real {ω | (B n ω).det = 0} = (1 - p + o n) ^ n := p:↑Ihp₀:0 < php₁:↑p ≤ 1 / 2Ω:ℕ → Type u_1mΩ:(n : ℕ) → MeasurableSpace (Ω n)P:(n : ℕ) → Measure (Ω n)B:(n : ℕ) → Ω n → Matrix (Fin n) (Fin n) ℝB_indep:∀ (n : ℕ), iIndepFun (fun x x_1 => B n x_1 x.1 x.2) (P n)B_bernoulli:∀ (n : ℕ) (i j : Fin n), HasLaw (fun x => B n x i j) Ber(1, 0, p) (P n)⊢ ∃ o, o =o[atTop] 1 ∧ ∀ n > 0, (P n).real {ω | (B n ω).det = 0} = (1 - ↑p + o n) ^ n
All goals completed! 🐙/--
This is the result stated in the paper's abstract:
For any sequence `Mₙ` of `n × n` random matrices with mutually independent `Rademacher` entries
we have that
`P(Mₙ is singular) = (1/2 + oₙ(1))ⁿ`.
-/
theorem declaration uses `sorry`corollary_2 {Ω : ℕ → Type*} (mΩ : ∀ n, MeasurableSpace (Ω n)) {P : (n : ℕ) → Measure (Ω n)}
{M : (n : ℕ) → Ω n → Matrix (Fin n) (Fin n) ℝ}
(M_indep : ∀ n, iIndepFun (fun x : Fin n × Fin n ↦ (M n · x.1 x.2)) (P n))
(M_rademacher : ∀ n i j, HasLaw (M n · i j) rademacherMeasure (P n)) :
∃ o : ℕ → ℝ, o =o[atTop] (1 : ℕ → ℝ) ∧
∀ n > 0, (P n).real {ω | (M n ω).det = 0} = (1 / 2 + o n) ^ n := Ω:ℕ → Type u_1mΩ:(n : ℕ) → MeasurableSpace (Ω n)P:(n : ℕ) → Measure (Ω n)M:(n : ℕ) → Ω n → Matrix (Fin n) (Fin n) ℝM_indep:∀ (n : ℕ), iIndepFun (fun x x_1 => M n x_1 x.1 x.2) (P n)M_rademacher:∀ (n : ℕ) (i j : Fin n), HasLaw (fun x => M n x i j) rademacherMeasure (P n)⊢ ∃ o, o =o[atTop] 1 ∧ ∀ n > 0, (P n).real {ω | (M n ω).det = 0} = (1 / 2 + o n) ^ n
All goals completed! 🐙
Hardy–Littlewood sign-change for the prime race mod 4
chebyshev_sign_change
#31
Verso theorem preview
theorem declaration uses `sorry`chebyshev_sign_change :
LeanEval.NumberTheory.ChebyshevSignChangeProblem.chebyshevLead.Infinite ∧
{n : ℕ | primeCountingMod 3 n < primeCountingMod 1 n}.Infinite := ⊢ chebyshevLead.Infinite ∧ {n | primeCountingMod 3 n < primeCountingMod 1 n}.Infinite
All goals completed! 🐙
Existence of a chiral oriented knot
exists_chiral_knot
#32
Verso theorem preview
theorem declaration uses `sorry`exists_chiral_knot : ∃ K : LeanEval.KnotTheory.Knot, K.Chiral := ⊢ ∃ K, K.Chiral
All goals completed! 🐙
Hopf–Rinow theorem
hopf_rinow
#33
Verso theorem preview
theorem declaration uses `sorry`hopf_rinow {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H)
[I.Boundaryless]
(M : Type*) [EMetricSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
[Bundle.RiemannianBundle (fun x : M => TangentSpace I x)]
[IsContMDiffRiemannianBundle I ∞ E (fun x : M => TangentSpace I x)]
[IsContinuousRiemannianBundle E (fun x : M => TangentSpace I x)]
[IsRiemannianManifold I M]
[LocallyCompactSpace M] [ConnectedSpace M] :
LeanEval.Geometry.IsGeodesicallyComplete M ↔ CompleteSpace M := E:Type u_1inst✝¹³:NormedAddCommGroup Einst✝¹²:NormedSpace ℝ Einst✝¹¹:FiniteDimensional ℝ EH:Type u_2inst✝¹⁰:TopologicalSpace HI:ModelWithCorners ℝ E Hinst✝⁹:I.BoundarylessM:Type u_3inst✝⁸:EMetricSpace Minst✝⁷:ChartedSpace H Minst✝⁶:IsManifold I ∞ Minst✝⁵:RiemannianBundle fun x => TangentSpace I xinst✝⁴:IsContMDiffRiemannianBundle I ∞ E fun x => TangentSpace I xinst✝³:IsContinuousRiemannianBundle E fun x => TangentSpace I xinst✝²:IsRiemannianManifold I Minst✝¹:LocallyCompactSpace Minst✝:ConnectedSpace M⊢ IsGeodesicallyComplete M ↔ CompleteSpace M
All goals completed! 🐙
Hessian estimates for the sigma-2 equation in dimension four
annals_hessian_estimates
#34
Verso theorem preview
theorem declaration uses `sorry`theorem_1_1 : ∃ C : ℝ≥0∞ → ℝ, ∀ (u : ℝ⁴ → ℝ)
(_smooth : ContDiffOn ℝ ∞ u B₁(0))
(_bounded : ‖u‖_C¹(B₁(0)) < (∞ : ℝ≥0∞))
(_positive_branch : ∀ x ∈ B₁(0), (Δ u) x > 0)
(_solution : ∀ x ∈ B₁(0), σ₂ (H u B₁(0) x) = 1),
‖H u B₁(0) 0‖_F ≤ C (‖u‖_C¹(B₁(0))) := ⊢ ∃ C,
∀ (u : ℝ⁴ → ℝ),
ContDiffOn ℝ ∞ u B₁(0) →
‖u‖_C¹(B₁(0)) < ∞ →
(∀ x ∈ B₁(0), Δ u x > 0) → (∀ x ∈ B₁(0), σ₂ (H u B₁(0) x) = 1) → ‖H u B₁(0) 0‖_F ≤ C ‖u‖_C¹(B₁(0))
All goals completed! 🐙
Schmidt's subspace theorem
schmidt_subspace
#35
Verso theorem preview
theorem declaration uses `sorry`schmidt_subspace (σ : Type*) [Fintype σ] (hσ : 2 ≤ Fintype.card σ)
(L : σ → σ → ℂ)
(alg : ∀ i j, IsAlgebraic ℚ (L i j)) (ind : LinearIndependent ℂ L)
(ε : ℝ) (pos : 0 < ε) :
∃ s : Finset (σ → ℤ), 0 ∉ s ∧ ∀ x : σ → ℤ,
‖∏ i, ∑ j, L i j * x j‖ < ‖x‖ ^ (-ε) → ∃ c ∈ s, ∑ i, c i * x i = 0 := σ:Type u_1inst✝:Fintype σhσ:2 ≤ Fintype.card σL:σ → σ → ℂalg:∀ (i j : σ), IsAlgebraic ℚ (L i j)ind:LinearIndependent ℂ Lε:ℝpos:0 < ε⊢ ∃ s, 0 ∉ s ∧ ∀ (x : σ → ℤ), ‖∏ i, ∑ j, L i j * ↑(x j)‖ < ‖x‖ ^ (-ε) → ∃ c ∈ s, ∑ i, c i * x i = 0
All goals completed! 🐙
Szemerédi's theorem
szemeredi
#36
Verso theorem preview
theorem declaration uses `sorry`szemeredi (A : Set ℕ) (h : 0 < upperDensity A) :
LeanEval.Combinatorics.ContainsArbitraryAPs A := A:Set ℕh:0 < upperDensity A⊢ ContainsArbitraryAPs A
All goals completed! 🐙
Vinogradov mean value theorem
vinogradov_mean_value
#37
Verso theorem preview
theorem declaration uses `sorry`vinogradov_mean_value (s k : ℕ) (ε : ℝ) (hε : 0 < ε) :
LeanEval.NumberTheory.VinogradovMeanValue.J s k =O[Filter.atTop]
fun X ↦ (X ^ (s + ε) + X ^ ((2 * s : ℝ) - k * (k + 1) / 2 + ε) : ℝ) := s:ℕk:ℕε:ℝhε:0 < ε⊢ J s k =O[Filter.atTop] fun X => ↑X ^ (↑s + ε) + ↑X ^ (2 * ↑s - ↑k * (↑k + 1) / 2 + ε)
All goals completed! 🐙
Equiangular lines with a fixed angle
annals_equiangular_lines_fixed_angle
#38
Verso theorem preview
theorem declaration uses `sorry`theorem_1_2 (α : ℝ) (hα : α ∈ Set.Ioo 0 1) :
let k := spectralRadiusOrder ((1 - α) / (2 * α))
(k < ⊤ → ∀ᶠ d in atTop, N α d = ⌊(k.toNat * (d - 1) : ℝ) / (k.toNat - 1 : ℝ)⌋₊) ∧
(k = ⊤ → ∃ e : ℕ → ℝ, e =o[atTop] (Nat.cast : ℕ → ℝ) ∧ ∀ d, N α d = d + e d) := α:ℝhα:α ∈ Set.Ioo 0 1⊢ let k := spectralRadiusOrder ((1 - α) / (2 * α));
(k < ⊤ → ∀ᶠ (d : ℕ) in atTop, N α d = ⌊↑k.toNat * (↑d - 1) / (↑k.toNat - 1)⌋₊) ∧
(k = ⊤ → ∃ e, e =o[atTop] Nat.cast ∧ ∀ (d : ℕ), ↑(N α d) = ↑d + e d)
All goals completed! 🐙
Rademacher type and Enflo type coincide
annals_rademacher_enflo_type
#39
Lean theorem statement
/--
Statement of Theorem 1.1:
For any `p ∈ [1,2]`, and Banach space `X`
`TRₚ(X) ≤ TEₚ(X) ≤ (π / √2) TRₚ(X)`.
-/
theorem theorem_1_1 (p : ℝ) (h1p : 1 ≤ p) (hp2 : p ≤ 2) :
TR X p ≤ TE X p ∧ TE X p ≤ (pi / sqrt 2) * TR X p := by
sorry
Glauberman's Z* theorem for isolated involutions
glauberman_zStar
#40
Verso theorem preview
theorem declaration uses `sorry`glauberman_zStar (G : Type) [Group G] [Fintype G]
(t : G) (ht1 : t ≠ 1) (ht2 : t * t = 1)
(hisolated : ∀ g : G, (g * t * g⁻¹) * t = t * (g * t * g⁻¹) →
g * t * g⁻¹ = t) :
∃ N : Subgroup G, N.Normal ∧ Odd (Nat.card N) ∧
∀ g : G, g * t * g⁻¹ * t⁻¹ ∈ N := G:Typeinst✝¹:Group Ginst✝:Fintype Gt:Ght1:t ≠ 1ht2:t * t = 1hisolated:∀ (g : G), g * t * g⁻¹ * t = t * (g * t * g⁻¹) → g * t * g⁻¹ = t⊢ ∃ N, N.Normal ∧ Odd (Nat.card ↥N) ∧ ∀ (g : G), g * t * g⁻¹ * t⁻¹ ∈ N
All goals completed! 🐙
Schläfli classification of regular polytopes
schlafli_classification
#41
Verso theorem preview
theorem declaration uses `sorry`schlafli_classification :
platonicCount 3 = 5 ∧
platonicCount 4 = 6 ∧
∀ d, 5 ≤ d → platonicCount d = 3 := ⊢ platonicCount 3 = 5 ∧ platonicCount 4 = 6 ∧ ∀ (d : ℕ), 5 ≤ d → platonicCount d = 3
All goals completed! 🐙
On the Duffin-Schaeffer conjecture
annals_duffin_schaeffer_conjecture
#42
Verso theorem preview
/--
Statement of Theorem 1:
If for `ψ : ℕ → ℝ≥0`, the infinite series `∑ (ψ q * φ q) / q`, where `φ` is the
Euler totient function, diverges, then the set `𝒜` defined above has Lebesgue measure `1`.
-/
theorem declaration uses `sorry`theorem_1 (ψ : ℕ+ → ℝ≥0) (hdivergence : ¬ Summable fun q ↦ (ψ q * φ q) / q) :
MeasurableSet (𝒜 ψ) ∧ volume (𝒜 ψ) = 1 := ψ:ℕ+ → ℝ≥0hdivergence:¬Summable fun q => ψ q * ↑(φ ↑q) / ↑↑q⊢ MeasurableSet (𝒜 ψ) ∧ volume (𝒜 ψ) = 1
All goals completed! 🐙/--
Statement of Theorem 2(a):
Let `ψ : ℕ → ℝ≥0`, `𝒦` and `ψ⋆` be as above. Then, if `∑ ψ⋆ (q)` converges, `𝒦` has Lebesgue
measure `0`.
-/
theorem declaration uses `sorry`theorem_2_a (ψ : ℕ+ → ℝ≥0) (hψ : ∑' q, ψ_star ψ q < ∞) :
MeasurableSet (𝒦 ψ) ∧ volume (𝒦 ψ) = 0 := ψ:ℕ+ → ℝ≥0hψ:∑' (q : ℕ+), ψ_star ψ q < ∞⊢ MeasurableSet (𝒦 ψ) ∧ volume (𝒦 ψ) = 0
All goals completed! 🐙/--
Statement of Theorem 2(b):
Let `ψ : ℕ → ℝ≥0`, `𝒦` and `ψ⋆` be as above. Then, if `∑ ψ⋆ (q)` diverges, `𝒦` has Lebesgue
measure `1`.
-/
theorem declaration uses `sorry`theorem_2_b (ψ : ℕ+ → ℝ≥0) (hψ : ∑' q, ψ_star ψ q = ∞) :
MeasurableSet (𝒦 ψ) ∧ volume (𝒦 ψ) = 1 := ψ:ℕ+ → ℝ≥0hψ:∑' (q : ℕ+), ψ_star ψ q = ∞⊢ MeasurableSet (𝒦 ψ) ∧ volume (𝒦 ψ) = 1
All goals completed! 🐙/--
Statement of Corollary 3:
For a function `ψ : ℕ → [0, 1/2]`, the set `𝒜` and the element `s` defined as above,
the Hausdorff dimension of `𝒜` is the minimum of `s` and `1`.
-/
theorem declaration uses `sorry`corollary_3 (ψ : ℕ+ → ℝ≥0) (hψ : ∀ n, ψ n ∈ Set.Icc 0 (1 / 2)) :
dimH (𝒜 ψ) = min (s_inf ψ) 1 := ψ:ℕ+ → ℝ≥0hψ:∀ (n : ℕ+), ψ n ∈ Set.Icc 0 (1 / 2)⊢ dimH (𝒜 ψ) = ↑(min (s_inf ψ) 1)
All goals completed! 🐙
A reverse Minkowski theorem
annals_reverse_minkowski
#43
Verso theorem preview
theorem declaration uses `sorry`theorem_1_2 (ℒ : Submodule ℤ ℝⁿ) [DiscreteTopology ℒ] (hℒ : IsZLattice ℝ ℒ)
(h : ∀ ℒ' (_hℒℒ' : ℒ' ≤ ℒ) [DiscreteTopology ℒ'], determinant ℒ' ≥ 1) :
let t : ℝ := 10 * (log n + 2)
ρ (1 / t) ℒ ≤ 3 / 2 := n:ℕℒ:Submodule ℤ ℝⁿinst✝:DiscreteTopology ↥ℒhℒ:IsZLattice ℝ ℒh:∀ ℒ' ≤ ℒ, ∀ [inst : DiscreteTopology ↥ℒ'], determinant ℒ' ≥ 1⊢ let t := 10 * (log ↑n + 2);
ρ (1 / t) ℒ ≤ 3 / 2
All goals completed! 🐙
Duffin-Schaeffer conjecture
duffin_schaeffer
#44
Lean theorem statement
/-- **Koukoulopoulos-Maynard theorem (Duffin-Schaeffer conjecture).** For nonnegative
approximation radii `delta`, the corresponding limsup set of reduced
rational approximations has full measure exactly when
`sum_n phi(n) * delta(n)` diverges. -/
theorem duffin_schaeffer (δ : ℕ → ℝ) (hδ : ∀ n, 0 ≤ δ n) :
volume (addWellApproximable UnitAddCircle δ) = 1 ↔
¬ Summable fun n : ℕ => n.totient * δ n := by
sorry
Thresholds versus fractional expectation-thresholds
annals_fractional_expectation_thresholds
#45
Verso theorem preview
/-- The constant `K` in Theorem 1.1. -/
noncomputable def declaration uses `sorry`K : ℝ := sorry/--
Statement of Theorem 1.1:
There exists a universal constant `K` such that for any finite set `X` and any increasing
collection of sets `𝓕` such that `l(𝓕)` is at least `2`,
`p_c(𝓕) ≤ K * q_f(𝓕) * log l(𝓕)`.
Note: The assumption that `l(𝓕)` is at least `2` is not explicitly in the paper but is needed
because if `l(𝓕) = 1` then `Real.log (l 𝓕) = 0`, but `p_c 𝓕 ∈ (0,1)` (so the inequality clearly
cannot hold).
-/
theorem declaration uses `sorry`theorem_1_1 (X : Type*) [Fintype X] (𝓕 : Set (Set X)) (h𝓕 : IsUpperSet 𝓕)
(hl𝓕 : 2 ≤ l 𝓕) : p_c 𝓕 ≤ K * q_f 𝓕 * Real.log (l 𝓕) := X:Type u_1inst✝:Fintype X𝓕:Set (Set X)h𝓕:IsUpperSet 𝓕hl𝓕:2 ≤ l 𝓕⊢ ↑(p_c 𝓕) ≤ K * ↑(q_f 𝓕) * Real.log ↑(l 𝓕)
All goals completed! 🐙
Rational approximations to linear subspaces
annals_linear_subspaces
#46
Verso theorem preview
theorem declaration uses `sorry`theorem_1 (hd : 2 ≤ d) (l : ℕ) (hl0 : 0 < l) (hld : l < d) (k : ℕ) (hk1 : 1 ≤ k) (hkl : k ≤ l) :
(∀ x : Submodule ℝ ℝᵈ, finrank ℝ x = l → LinearSubspaces.diophantineExponent k x ≥ d / (k * (d - l))) ∧
(∃ x : Submodule ℝ ℝᵈ, finrank ℝ x = l ∧ LinearSubspaces.diophantineExponent k x = d / (k * (d - l))) := d:ℕhd:2 ≤ dl:ℕhl0:0 < lhld:l < dk:ℕhk1:1 ≤ khkl:k ≤ l⊢ (∀ (x : Submodule ℝ ℝᵈ), finrank ℝ ↥x = l → diophantineExponent k x ≥ ↑d / (↑k * (↑d - ↑l))) ∧
∃ x, finrank ℝ ↥x = l ∧ diophantineExponent k x = ↑d / (↑k * (↑d - ↑l))
All goals completed! 🐙
The local-global conjecture for Apollonian circle packings is false
annals_local_global_apollonian_circle_packings
#47
Verso theorem preview
/--
Statement of Theorem 1.6:
The Apollonian circle packing `A` generated by `(−3, 5, 8, 8)` has no square curvatures.
-/
theorem declaration uses `sorry`theorem_1_6 : ∀ n, n ^ 2 ∉ curvatureSet ⟦⟨![-3, 5, 8, 8], n:ℤ⊢ ![-3, 5, 8, 8] ∈ integralPrimitiveDescartesQuadruple All goals completed! 🐙⟩⟧ := ⊢ ∀ (n : ℤ), n ^ 2 ∉ curvatureSet ⟦⟨![-3, 5, 8, 8], ⋯⟩⟧
All goals completed! 🐙/--
Statement of Theorem 1.3:
There exist infinitely many `A` for which the number of missing curvatures up to `N` is `Ω(√N)`.
-/
theorem declaration uses `sorry`theorem_1_3 : {A : PrimitiveApollonianCirclePacking |
Real.sqrt =O[Filter.atTop] missingCurvatures A}.Infinite := ⊢ {A | Real.sqrt =O[Filter.atTop] missingCurvatures A}.Infinite
All goals completed! 🐙
The optimal paper Moebius band
annals_optimal_moebius
#48
Verso theorem preview
theorem declaration uses `sorry`theorem_1_1 (a : ℝ) (ha : a > 0) (f : ℝ² → ℝ³) (hf : OptimalMoebius.IsMoebiusEmbedding a f) :
a > √3 := a:ℝha:a > 0f:ℝ² → ℝ³hf:IsMoebiusEmbedding a f⊢ a > √3
All goals completed! 🐙
Neukirch–Uchida theorem
neukirch_uchida
#49
Verso theorem preview
theorem declaration uses `sorry`neukirch_uchida {K₁ K₂ K₁' K₂' : Type*} [Field K₁] [Field K₂] [Field K₁'] [Field K₂']
[NumberField K₁] [NumberField K₂] [Algebra K₁ K₁'] [Algebra K₂ K₂'] [IsSepClosure K₁ K₁']
[IsSepClosure K₂ K₂'] (ϕ : Gal(K₁'/K₁) ≃* Gal(K₂'/K₂)) (he : IsHomeomorph ϕ) :
∃! σ : K₂' ≃+* K₁', (algebraMap K₂ K₂').range.map σ.toRingHom = (algebraMap K₁ K₁').range ∧
∀ g : Gal(K₁'/K₁), ϕ g = σ.trans (g.toRingEquiv.trans σ.symm) := K₁:Type u_1K₂:Type u_2K₁':Type u_3K₂':Type u_4inst✝⁹:Field K₁inst✝⁸:Field K₂inst✝⁷:Field K₁'inst✝⁶:Field K₂'inst✝⁵:NumberField K₁inst✝⁴:NumberField K₂inst✝³:Algebra K₁ K₁'inst✝²:Algebra K₂ K₂'inst✝¹:IsSepClosure K₁ K₁'inst✝:IsSepClosure K₂ K₂'ϕ:Gal(K₁'/K₁) ≃* Gal(K₂'/K₂)he:IsHomeomorph ⇑ϕ⊢ ∃! σ,
Subring.map σ.toRingHom (algebraMap K₂ K₂').range = (algebraMap K₁ K₁').range ∧
∀ (g : Gal(K₁'/K₁)), (ϕ g).toRingEquiv = σ.trans (g.toRingEquiv.trans σ.symm)
All goals completed! 🐙
Algebraic integers with conjugates in a prescribed distribution
annals_algebraic_integers
#50
Verso theorem preview
theorem declaration uses `sorry`theorem_1_1 : lambda_SSS < 1.89831 := ⊢ lambda_SSS < 1.89831
All goals completed! 🐙
Hadwiger's theorem
hadwiger
#51
Verso theorem preview
theorem declaration uses `sorry`hadwiger (n : ℕ) : Module.finrank ℝ (valuations n) = n + 1 := n:ℕ⊢ Module.finrank ℝ ↥(valuations n) = n + 1
All goals completed! 🐙
pi_(n+1) of S^n is Z/2 for n at least 3
pi_succ_sphere_n_mulEquiv_zmod_two
#52
Verso theorem preview
theorem declaration uses `sorry`pi_succ_sphere_n_mulEquiv_zmod_two (n : ℕ) (hn : 3 ≤ n)
(x : Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1) :
Nonempty
(HomotopyGroup.Pi (n + 1) (Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1) x ≃*
Multiplicative (ZMod 2)) := n:ℕhn:3 ≤ nx:↑(Metric.sphere 0 1)⊢ Nonempty (HomotopyGroup.Pi (n + 1) (↑(Metric.sphere 0 1)) x ≃* Multiplicative (ZMod 2))
All goals completed! 🐙
Coherent cohomology of a proper scheme over ℚ is finite-dimensional
coherent_cohomology_finite_dimensional
#53
Verso theorem preview
theorem declaration uses `sorry`coherent_cohomology_finite_dimensional (f : X ⟶ Spec (CommRingCat.of ℚ)) [IsProper f]
[M.IsFiniteType] [M.IsQuasicoherent] (n : ℕ) :
Module.Finite ℚ (ℚ ⊗[ℤ] M.sheaf.H n) := X:SchemeM:X.Modulesf:X ⟶ Spec (CommRingCat.of ℚ)inst✝²:IsProper finst✝¹:SheafOfModules.IsFiniteType Minst✝:SheafOfModules.IsQuasicoherent Mn:ℕ⊢ Module.Finite ℚ (ℚ ⊗[ℤ] Sheaf.H Scheme.Modules.sheaf n)
All goals completed! 🐙
Fatou–Julia / Cantor dichotomy
fatou_julia_dichotomy
#54
Lean theorem statement
/-- **Fatou–Julia dichotomy.** For the quadratic family, `c ∈ M` implies
the filled Julia set `K_c` is connected; `c ∉ M` implies `K_c` is
homeomorphic to the Cantor space `ℕ → Bool`. -/
theorem julia_cantor_dichotomy (c : ℂ) :
(c ∈ Mandelbrot → IsConnected (FilledJulia c)) ∧
(c ∉ Mandelbrot → Nonempty ((FilledJulia c) ≃ₜ (ℕ → Bool))) := by
sorry
Connective constant of the honeycomb lattice
honeycomb_connective_constant
#55
Verso theorem preview
theorem declaration uses `sorry`honeycomb_connective_constant :
Tendsto
(fun n ↦ (LeanEval.Combinatorics.HoneycombConnectiveConstant.walkCount n : ℝ) ^ (1 / n : ℝ))
atTop
(nhds (Real.sqrt (2 + Real.sqrt 2))) := ⊢ Tendsto (fun n => ↑(walkCount n) ^ (1 / ↑n)) atTop (𝓝 √(2 + √2))
All goals completed! 🐙
Novikov's theorem: the word problem is undecidable for finitely presented groups
novikov_unsolvable
#56
Lean theorem statement
/-- **Novikov's theorem** (P.S. Novikov 1955; independently W.W. Boone
1958). There exists a finite presentation with undecidable word
problem. -/
theorem novikov_unsolvable :
∃ (n : ℕ) (rels : Set (FreeGroup (Fin n))),
rels.Finite ∧ ¬ WordProblemSolvable (PresentedGroup.mk rels) := by
sorry
The alternating sign matrix theorem
alternating_sign_matrix_count
#57
Lean theorem statement
/-- **Alternating sign matrix theorem.** The number of `n × n` ASMs equals the
Robbins product. -/
theorem alternating_sign_matrix_count (n : ℕ) :
(Nat.card (ASMatrix n) : ℚ) = robbinsProduct n := by
sorry
A counterexample to the unit conjecture for group rings
annals_unit_conjecture
#58
Verso theorem preview
theorem declaration uses `sorry`theorem_A : (∀ g : UnitConjecture.P, ∀ n ≠ 0, g ^ n = 1 → g = 1) ∧ IsUnit UnitConjecture.u ∧ ¬ ∃ g : UnitConjecture.P, UnitConjecture.u = g := ⊢ (∀ (g : P) (n : ℕ), n ≠ 0 → g ^ n = 1 → g = 1) ∧ IsUnit u ∧ ¬∃ g, u = (MonoidAlgebra.of (ZMod 2) P) g
All goals completed! 🐙
Commuting probabilities are closed
commProb_closed
#59
Lean theorem statement
/-- The set of commuting probabilities of finite groups is closed. -/
theorem commProb_closed : IsClosed ({p : ℝ | ∃ (G : Type) (hG : Group G), commProb G = p}) := by
sorry
Conway–Schneeberger fifteen theorem
conway_schneeberger_fifteen
#60
Verso theorem preview
theorem declaration uses `sorry`conway_schneeberger_fifteen {n : ℕ}
(Q : Matrix (Fin n) (Fin n) ℤ)
(_hpos : Q.PosDef) :
LeanEval.NumberTheory.ConwaySchneebergerFifteenProblem.IsUniversal Q ↔ ∀ k ∈ Finset.Icc (1 : ℤ) 15, LeanEval.NumberTheory.ConwaySchneebergerFifteenProblem.Represents Q k := n:ℕQ:Matrix (Fin n) (Fin n) ℤ_hpos:Q.PosDef⊢ IsUniversal Q ↔ ∀ k ∈ Finset.Icc 1 15, Represents Q k
All goals completed! 🐙
Jacobian of a compact Riemann surface (Buzzard challenge)
jacobian_challenge_diffgeo
#61
Verso theorem preview
def declaration uses `sorry`genus (X : Type u) [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
[Nonempty X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ω X] : ℕ := sorrytheorem declaration uses `sorry`genus_eq_zero_iff_homeo :
genus X = 0 ↔ Nonempty (X ≃ₜ (Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1)) :=
sorrydef declaration uses `sorry`Jacobian (X : Type u) [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
[Nonempty X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ω X] : Type u := sorryinstance declaration uses `sorry`instAddCommGroup : AddCommGroup (Jacobian X) := sorryinstance declaration uses `sorry`instTopologicalSpace : TopologicalSpace (Jacobian X) := sorryinstance declaration uses `sorry`instT2Space : T2Space (Jacobian X) := sorryinstance declaration uses `sorry`instCompactSpace : CompactSpace (Jacobian X) := sorryinstance declaration uses `sorry`instChartedSpace : ChartedSpace (Fin (genus X) → ℂ) (Jacobian X) := sorryinstance declaration uses `sorry`instIsManifold :
IsManifold (modelWithCornersSelf ℂ (Fin (genus X) → ℂ)) ω (Jacobian X) := sorryinstance declaration uses `sorry`instLieAddGroup :
LieAddGroup (modelWithCornersSelf ℂ (Fin (genus X) → ℂ)) ω (Jacobian X) := sorrydef declaration uses `sorry`ofCurve (P : X) : X → Jacobian X := sorrytheorem declaration uses `sorry`ofCurve_contMDiff (P : X) :
ContMDiff (modelWithCornersSelf ℂ ℂ)
(modelWithCornersSelf ℂ (Fin (genus X) → ℂ)) ω (ofCurve P) := sorrytheorem declaration uses `sorry`ofCurve_self (P : X) : ofCurve P P = 0 := sorrytheorem declaration uses `sorry`ofCurve_inj (P : X) (h : 0 < genus X) : Function.Injective (ofCurve P) := sorrydef declaration uses `sorry`pushforward (f : X → Y)
(hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f) :
Jacobian X →ₜ+ Jacobian Y := sorrytheorem declaration uses `sorry`pushforward_contMDiff (f : X → Y)
(hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f) :
ContMDiff (modelWithCornersSelf ℂ (Fin (genus X) → ℂ))
(modelWithCornersSelf ℂ (Fin (genus Y) → ℂ)) ω (pushforward f hf) := sorrytheorem declaration uses `sorry`pushforward_id_apply (P : Jacobian X) :
pushforward id contMDiff_id P = P := sorrytheorem declaration uses `sorry`pushforward_comp_apply (f : X → Y)
(hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f)
(g : Y → Z) (hg : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω g)
(P : Jacobian X) :
pushforward (g ∘ f) (hg.comp hf) P = pushforward g hg (pushforward f hf P) :=
sorrydef declaration uses `sorry`pullback (f : X → Y)
(hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f) :
Jacobian Y →ₜ+ Jacobian X := sorrytheorem declaration uses `sorry`pullback_contMDiff (f : X → Y)
(hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f) :
ContMDiff (modelWithCornersSelf ℂ (Fin (genus Y) → ℂ))
(modelWithCornersSelf ℂ (Fin (genus X) → ℂ)) ω (pullback f hf) := sorrytheorem declaration uses `sorry`pullback_id_apply (P : Jacobian X) :
pullback id contMDiff_id P = P := sorrytheorem declaration uses `sorry`pullback_comp_apply (f : X → Y)
(hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f)
(g : Y → Z) (hg : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω g)
(P : Jacobian Z) :
pullback (g.comp f) (hg.comp hf) P = pullback f hf (pullback g hg P) := sorrydef declaration uses `sorry`degree (f : X → Y)
(hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f) : ℕ :=
sorry -- 0 for constant casetheorem declaration uses `sorry`pushforward_pullback (f : X → Y)
(hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f)
(P : Jacobian Y) :
pushforward f hf (pullback f hf P) = (degree f hf) • P := sorry
Poincaré–Bendixson theorem
poincare_bendixson
#62
Lean theorem statement
/-- **Poincaré–Bendixson theorem.** For a `C¹` autonomous vector field
`F : ℝ² → ℝ²` and a forward integral curve `γ` on `[0, ∞)`, either the
forward orbit is unbounded, or the ω-limit set contains an equilibrium
of `F`, or the ω-limit set equals the range of a non-constant periodic
integral curve of `F`. -/
theorem poincare_bendixson
(F : Plane → Plane) (_hF : ContDiff ℝ 1 F)
(γ : ℝ → Plane)
(_hγ : IsIntegralCurveOn γ (fun _ x => F x) (Set.Ici 0)) :
¬ Bornology.IsBounded (γ '' Set.Ici 0)
∨ (∃ x₀, F x₀ = 0 ∧ x₀ ∈ ⋂ s : ℝ, closure (γ '' Set.Ici s))
∨ (∃ T : ℝ, 0 < T ∧ ∃ β : ℝ → Plane,
IsIntegralCurve β (fun _ x => F x) ∧
(∀ t, β (t + T) = β t) ∧
F (β 0) ≠ 0 ∧
(⋂ s : ℝ, closure (γ '' Set.Ici s)) = Set.range β) := by
sorry
Thue–Siegel–Roth theorem (irrationality measure ≤ 2 for algebraic irrationals)
thue_siegel_roth
#63
Lean theorem statement
/-- **Thue–Siegel–Roth theorem** (Klaus Roth, 1955). Every irrational
algebraic real is Diophantine: its irrationality measure is at most
`2`. -/
theorem thueSiegelRoth (x : ℝ) (_h_irr : Irrational x)
(_h_alg : IsAlgebraic ℤ x) : IsDiophantine x := by
sorry
Weak Morse inequalities
weak_morse_inequality
#64
Lean theorem statement
/-- **Weak Morse inequalities.** For a Morse function `f` on a closed
smooth finite-dimensional Hausdorff manifold `M` and every `k ∈ ℕ`,
`b_k(M) ≤ c_k(f)`. -/
theorem weak_morse_inequality
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
{H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless]
{M : Type} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
[CompactSpace M] [T2Space M] (f : M → ℝ) (_hf : IsMorseFunction I f) (k : ℕ) :
bettiNumber M k ≤ morseCount I f k := by
sorry
Gleason's theorem (separable Hilbert space)
gleason_theorem_separable
#65
Lean theorem statement
/-- **Gleason's theorem**, separable Hilbert space version (Gleason's original 1957
formulation). For a separable complex Hilbert space `H` of dimension at least `3`, every
frame function on the unit sphere of `H` is given by `x ↦ re ⟨x, ρ x⟩` for some positive
bounded operator `ρ`. (The Lean conclusion does not separately assert trace-class /
`Tr ρ = 1`; see the file docstring.) -/
theorem gleason_theorem_separable
{H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
[CompleteSpace H] [TopologicalSpace.SeparableSpace H]
(hdim : 3 ≤ Module.rank ℂ H)
(f : SphereFrameFunction H) :
∃ ρ : H →L[ℂ] H,
ContinuousLinearMap.IsPositive ρ ∧
∀ x : Metric.sphere (0 : H) 1,
f.f x = (inner ℂ (x : H) (ρ (x : H))).re := by
sorry
Higman's infinite finitely-presented simple group
higman_infinite_simple
#66
Lean theorem statement
/-- **Higman's infinite simple group** (G. Higman 1951/1974). There
exists an infinite finitely presented simple group. -/
theorem higman_infinite_simple :
∃ (n : ℕ) (rels : Set (FreeGroup (Fin n))),
rels.Finite ∧ IsSimpleGroup (PresentedGroup rels) ∧
Infinite (PresentedGroup rels) := by
sorry
Platonic classification
platonic_classification
#67
Verso theorem preview
theorem declaration uses `sorry`platonic_classification :
platonicCount 2 = ⊤ ∧
platonicCount 3 = 5 ∧
platonicCount 4 = 6 ∧
∀ d, 5 ≤ d → platonicCount d = 3 := ⊢ platonicCount 2 = ⊤ ∧ platonicCount 3 = 5 ∧ platonicCount 4 = 6 ∧ ∀ (d : ℕ), 5 ≤ d → platonicCount d = 3
All goals completed! 🐙
Seventeen wallpaper groups (Pólya–Niggli 1924)
wallpaper_groups_17
#68
Lean theorem statement
/-- **There are exactly 17 wallpaper groups** (Pólya–Niggli 1924). -/
theorem there_are_17_wallpaper_groups :
crystallographicCount 2 = 17 := by
sorry
Ado–Iwasawa theorem over an arbitrary field
adoIwasawa
#69
Verso theorem preview
theorem declaration uses `sorry`adoIwasawa [FiniteDimensional K L] :
∃ (V : Type u) (_ : AddCommGroup V) (_ : Module K V) (_ : FiniteDimensional K V)
(ρ : L →ₗ⁅K⁆ Module.End K V), Function.Injective ρ := K:Type uL:Type uinst✝³:Field Kinst✝²:LieRing Linst✝¹:LieAlgebra K Linst✝:FiniteDimensional K L⊢ ∃ V x x_1, ∃ (_ : FiniteDimensional K V), ∃ ρ, Function.Injective ⇑ρ
All goals completed! 🐙
Brauer's splitting field theorem
brauer_splitting_field
#70
Lean theorem statement
theorem brauer_splitting_field
(G : Type) [Group G] [Fintype G]
(V : Type) [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
(ρ : Representation ℂ G V) :
∃ (φ : CyclotomicField (Monoid.exponent G) ℚ →+* ℂ)
(W : Type) (_ : AddCommGroup W)
(_ : Module (CyclotomicField (Monoid.exponent G) ℚ) W)
(σ : Representation (CyclotomicField (Monoid.exponent G) ℚ) G W),
letI : Algebra (CyclotomicField (Monoid.exponent G) ℚ) ℂ := φ.toAlgebra
∃ (f : (ℂ ⊗[CyclotomicField (Monoid.exponent G) ℚ] W) ≃ₗ[ℂ] V),
∀ (g : G) (x : ℂ ⊗[CyclotomicField (Monoid.exponent G) ℚ] W),
f ((σ g).baseChange ℂ x) = ρ g (f x) := by
sorry
Schoenflies theorem
schoenflies
#71
Verso theorem preview
theorem declaration uses `sorry`schoenflies (r : Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 → EuclideanSpace ℝ (Fin 2))
(_hcont : Continuous r) (_hinj : Function.Injective r) :
∃ h : EuclideanSpace ℝ (Fin 2) ≃ₜ EuclideanSpace ℝ (Fin 2),
h '' Set.range r = Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 := r:↑(Metric.sphere 0 1) → EuclideanSpace ℝ (Fin 2)_hcont:Continuous r_hinj:Function.Injective r⊢ ∃ h, ⇑h '' Set.range r = Metric.sphere 0 1
All goals completed! 🐙
Fáry–Milnor theorem (knot total curvature ≤ 4π implies unknotted)
fary_milnor
#72
Lean theorem statement
/-- **Fáry–Milnor theorem** (Fáry 1949 / Milnor 1950). A smooth knot
with total curvature at most `4π` is unknotted. -/
theorem fary_milnor_total_curvature
{r : ℝ → Space} (_hknot : IsSmoothKnot r)
(_hK : totalCurvature r ≤ 4 * Real.pi) :
IsUnknotted r := by
sorry
Gleason's theorem (finite-dimensional)
gleason_theorem_finite
#73
Lean theorem statement
/-- **Gleason's theorem**, finite-dimensional version. For `dim H ≥ 3`, every frame
function on the projection lattice of `H` is given by `P ↦ re Tr(ρ P)` for the unique
density operator `ρ` (positive, `re Tr ρ = 1`). -/
theorem gleason_theorem_finite
{H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
[CompleteSpace H] [FiniteDimensional ℂ H]
(hdim : 3 ≤ Module.finrank ℂ H)
(f : FrameFunction H) :
∃! ρ : H →L[ℂ] H,
ContinuousLinearMap.IsPositive ρ ∧
reTr ρ = 1 ∧
∀ P : H →L[ℂ] H, IsOrthProj P → f.μ P = reTr (ρ * P) := by
sorry
Wieferich's theorem g(3) = 9
wieferich_g_three
#74
Lean theorem statement
/-- **Wieferich's theorem `g(3) = 9`.** Every natural number is a sum of nine
cubes, and nine is necessary: some `n` (namely `23`) is not a sum of eight
cubes. -/
theorem wieferich_g_three :
(∀ n : ℕ, IsSumOfCubes 9 n) ∧ ∃ n : ℕ, ¬ IsSumOfCubes 8 n := by
sorry
Margulis–Ruelle inequality
margulis_ruelle
#75
Lean theorem statement
/-- **Margulis–Ruelle inequality (1968/1978).** `h_μ(T) ≤ λ₁⁺ + λ₂⁺`. -/
theorem margulis_ruelle
(T T_inv : EucPlane → EucPlane)
(hT_smooth : ContDiff ℝ 2 T)
(hT_inv_smooth : ContDiff ℝ 2 T_inv)
(hT_left : Function.LeftInverse T_inv T)
(hT_right : Function.RightInverse T_inv T)
(K : Set EucPlane)
(hK_compact : IsCompact K)
(hK_inv : T '' K = K)
(μ : Measure EucPlane) [IsProbabilityMeasure μ]
(hμ_supp : μ Kᶜ = 0)
(hμ_pres : MeasurePreserving T μ μ)
(hμ_erg : Ergodic T μ) :
kolmogorovSinaiEntropy μ T
≤ max 0 (∫ x, lyapunovUpperAt T x ∂μ)
+ max 0 (∫ x, lyapunovLowerAt T x ∂μ) := by
sorry
Mergelyan's theorem
mergelyan_theorem
#76
Lean theorem statement
/-- **Mergelyan's theorem.** For a compact `K ⊆ ℂ` with connected
complement and `f : ℂ → ℂ` continuous on `K` and analytic on the
interior of `K`, every `ε > 0` admits a complex polynomial `p` with
`‖f z − p(z)‖ < ε` on `K`. -/
theorem mergelyan (K : Set ℂ) (_hK : IsCompact K) (_hKc : IsConnected (Kᶜ))
(f : ℂ → ℂ) (_hfc : ContinuousOn f K) (_hfh : AnalyticOnNhd ℂ f (interior K))
(ε : ℝ) (_hε : 0 < ε) :
∃ p : ℂ[X], ∀ z ∈ K, ‖f z - p.eval z‖ < ε := by
sorry
pi_n of the n-sphere is Z
pin_sphere_n_mulEquiv_int
#77
Lean theorem statement
/-- For every `n ≥ 1`, the `n`th homotopy group of the `n`-sphere is infinite cyclic. -/
theorem pin_sphere_n_mulEquiv_int
(n : ℕ)
(x : Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 2))) 1) :
Nonempty
(HomotopyGroup.Pi (n + 1) (Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 2))) 1) x ≃*
Multiplicative ℤ) := by
sorry
Brauer–Suzuki theorem (quaternion Sylow 2-subgroup)
brauer_suzuki
#78
Verso theorem preview
theorem declaration uses `sorry`brauer_suzuki {G : Type*} [Group G] [Finite G]
(n : ℕ) (hn : 3 ≤ n)
(P : Sylow 2 G)
(hquat : Nonempty ((P : Subgroup G) ≃* QuaternionGroup (2 ^ (n - 2))))
(t : G) (ht_mem : t ∈ (P : Subgroup G)) (ht_ord : orderOf t = 2) :
(QuotientGroup.mk t : G ⧸ LeanEval.GroupTheory.Defs.oddCore G) ∈
Subgroup.center (G ⧸ LeanEval.GroupTheory.Defs.oddCore G) := G:Type u_1inst✝¹:Group Ginst✝:Finite Gn:ℕhn:3 ≤ nP:Sylow 2 Ghquat:Nonempty (↥↑P ≃* QuaternionGroup (2 ^ (n - 2)))t:Ght_mem:t ∈ ↑Pht_ord:orderOf t = 2⊢ ↑t ∈ Subgroup.center (G ⧸ oddCore G)
All goals completed! 🐙
Dehn–Sommerville equations for simplicial spheres
dehn_sommerville
#79
Lean theorem statement
/-- **Dehn–Sommerville equations.** The h-vector of a finite simplicial sphere
is symmetric: `h_j = h_{d-j}`. -/
theorem dehn_sommerville
{d j : ℕ} (X : FiniteSimplicialSphere d) (hj : j ≤ d) :
hVector X j = hVector X (d - j) := by
sorry
Onsager's 2D Ising phase transition
ising_2d_phase_transition
#80
Lean theorem statement
/-- **Onsager's 2D Ising phase transition.** The thermodynamic-limit free
energy exists for all `β` and is non-analytic at some positive `βc`. -/
theorem ising_2d_phase_transition :
∃ (F : ℝ → ℝ) (βc : ℝ),
0 < βc ∧
(∀ β : ℝ,
Tendsto (fun n : ℕ => finiteIsingFreeEnergySeq n β) atTop (𝓝 (F β))) ∧
¬ AnalyticAt ℝ F βc := by
sorry
Jordan–Brouwer separation theorem
jordan_brouwer
#81
Lean theorem statement
/-- **Jordan–Brouwer separation theorem.** For `d ≥ 2`, the
complement in `ℝᵈ` of a topological `(d−1)`-sphere (the image of any
continuous injection from the unit `(d−1)`-sphere into `ℝᵈ`) has
exactly two connected components. -/
theorem jordan_brouwer (d : ℕ) (_hd : 2 ≤ d)
(r : Metric.sphere (0 : EuclideanSpace ℝ (Fin d)) 1 → EuclideanSpace ℝ (Fin d))
(_hcont : Continuous r) (_hinj : Function.Injective r) :
Nat.card
(ConnectedComponents ((Set.range r)ᶜ : Set (EuclideanSpace ℝ (Fin d)))) =
2 := by
sorry
Upper bound theorem for geometric simplicial spheres (Stanley 1975)
upper_bound_simplicial_spheres
#82
Lean theorem statement
/-- **Upper bound theorem for simplicial spheres** (Stanley 1975).
Every `k`-face count of a finite simplicial `(d − 1)`-sphere with `n`
vertices is bounded above by the corresponding face count of the
cyclic polytope `C(n, d)`. -/
theorem upper_bound_theorem_simplicial_spheres
{d n k : ℕ} (X : FiniteSimplicialSphere d)
(_hn : faceCount X 0 = n) (_hk : k < d) :
faceCount X k ≤ cyclicPolytopeFaceCount n d k := by
sorry
KAM persistence of an invariant curve
kam_invariant_curve
#83
Lean theorem statement
/-- **KAM theorem (persistence of an invariant curve).** For real-analytic,
`1`-periodic, non-constant, mean-zero `f` and Diophantine `α`, for all small
`|c|` the twist-map functional equation
`q(t+α) − 2q(t) + q(t−α) = c·f(q(t))` has a smooth strictly increasing solution
`q` with `q − id` periodic — the `c = 0` curve `q₀(t) = t` persists as a smooth
invariant curve of rotation number `α`. -/
theorem kam_invariant_curve
(α : ℝ) (_hα : IsDiophantine α)
(f : ℝ → ℝ)
(_hf_analytic : AnalyticOnNhd ℝ f Set.univ)
(_hf_per : Function.Periodic f 1)
(_hf_nonconst : ¬ ∃ k : ℝ, ∀ x, f x = k)
(_hf_mean : ∫ x in (0 : ℝ)..1, f x = 0) :
∃ c₀ : ℝ, 0 < c₀ ∧ ∀ c : ℝ, |c| < c₀ →
∃ q : ℝ → ℝ,
ContDiff ℝ ∞ q ∧ StrictMono q ∧
Function.Periodic (fun t => q t - t) 1 ∧
∀ t : ℝ, q (t + α) - 2 * q t + q (t - α) = c * f (q t) := by
sorry
Mandelbrot set is connected (Douady–Hubbard)
mandelbrot_connected
#84
Lean theorem statement
/-- **Mandelbrot set is connected** (Douady–Hubbard). -/ theorem mandelbrot_connected : IsConnected Mandelbrot := by sorry
pi_3 of the 2-sphere is Z
pi3_sphere_two_mulEquiv_int
#85
Lean theorem statement
/-- The third homotopy group of the 2-sphere is infinite cyclic. -/
theorem pi3_sphere_two_mulEquiv_int
(x : Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1) :
Nonempty
(HomotopyGroup.Pi 3 (Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1) x ≃*
Multiplicative ℤ) := by
sorry
Bézout's theorem (projective, with multiplicity)
bezout_projective_multiplicity
#86
Lean theorem statement
/-- **Bézout's theorem (with multiplicity).** Given `n` homogeneous
polynomials `f_k` in `n + 1` variables, each of total degree exactly
`d_k ≥ 1`, over an algebraically closed field with finite common
projective zero set, the sum of intersection multiplicities equals
`∏ d_k`. The `totalDegree` hypothesis rules out the zero polynomial
(which is `IsHomogeneous d` for every `d` but has `totalDegree = 0`). -/
theorem bezout_multiplicity [IsAlgClosed K] {n : ℕ}
(f : Fin n → MvPolynomial (Fin (n + 1)) K)
(d : Fin n → ℕ) (_hd : ∀ k, (f k).IsHomogeneous (d k))
(_hdeg : ∀ k, (f k).totalDegree = d k)
(_hd_pos : ∀ k, 1 ≤ d k)
(_hfin : (⋂ k, vanishingSet (f k)).Finite) :
∑ᶠ p ∈ (⋂ k, vanishingSet (f k)), intersectionMultiplicity f p
= (∏ k, d k : ℕ∞) := by
sorry
Furstenberg measure-preserving multiple recurrence
furstenberg_measure
#87
Verso theorem preview
theorem declaration uses `sorry`furstenberg_measure_recurrence {Ω : Type*}
[MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
{T : Ω → Ω} (_hT : MeasureTheory.MeasurePreserving T μ μ)
{A : Set Ω} (_hA : MeasurableSet A) (_h0 : 0 < μ A)
(d : ℕ) (_hd : 1 ≤ d) :
∃ n : ℕ, 1 ≤ n ∧
0 < μ (A ∩ ⋂ j ∈ Finset.Icc 1 d, T^[j * n] ⁻¹' A) := Ω:Type u_1inst✝¹:MeasurableSpace Ωμ:Measure Ωinst✝:IsProbabilityMeasure μT:Ω → Ω_hT:MeasurePreserving T μ μA:Set Ω_hA:MeasurableSet A_h0:0 < μ Ad:ℕ_hd:1 ≤ d⊢ ∃ n, 1 ≤ n ∧ 0 < μ (A ∩ ⋂ j ∈ Finset.Icc 1 d, T^[j * n] ⁻¹' A)
All goals completed! 🐙
Morse inequalities
morse_inequality
#88
Lean theorem statement
/-- **Morse inequalities** (Marston Morse, 1934). For a Morse function `f`
on a closed smooth finite-dimensional Hausdorff manifold `M` and every `k ∈ ℕ`,
`∑_{j≤k}(−1)^{k−j} c_j(f) ≥ ∑_{j≤k}(−1)^{k−j} b_j(M)`. -/
theorem morse_inequality
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
{H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless]
{M : Type} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
[CompactSpace M] [T2Space M] (f : M → ℝ) (_hf : IsMorseFunction I f) (k : ℕ) :
alternatingPartialSum (bettiNumber M) k ≤
alternatingPartialSum (morseCount I f) k := by
sorry
Strong Mason conjecture for matroid independent sets
strong_mason_conjecture
#89
Verso theorem preview
theorem declaration uses `sorry`strong_mason_conjecture {α : Type*} (M : Matroid α) [M.Finite]
(k : ℕ) (hk : 0 < k) (hkn : k < M.E.ncard) :
independentSetCount M (k - 1) * independentSetCount M (k + 1) *
(k + 1) * (M.E.ncard - k + 1) ≤
independentSetCount M k ^ 2 * k * (M.E.ncard - k) := α:Type u_1M:Matroid αinst✝:M.Finitek:ℕhk:0 < khkn:k < M.E.ncard⊢ independentSetCount M (k - 1) * independentSetCount M (k + 1) * (k + 1) * (M.E.ncard - k + 1) ≤
independentSetCount M k ^ 2 * k * (M.E.ncard - k)
All goals completed! 🐙
Spencer-Szemerédi-Trotter unit-distance upper bound
unit_distance_upper_bound
#90
Verso theorem preview
theorem declaration uses `sorry`unit_distance_upper_bound :
∃ C : ℝ, 0 < C ∧
∀ P : Finset (EuclideanSpace ℝ (Fin 2)),
(unitDist P : ℝ) ≤ C * (P.card : ℝ) ^ ((4 : ℝ) / 3) := ⊢ ∃ C, 0 < C ∧ ∀ (P : Finset (EuclideanSpace ℝ (Fin 2))), ↑(unitDist P) ≤ C * ↑P.card ^ (4 / 3)
All goals completed! 🐙
Existence of a simple group of order 10200960 with a 22-dim irrep whose tensor square has 4 isotypic components
m23_irrep_tensor_square_decomp
#91
Verso theorem preview
theorem declaration uses `sorry`m23_irrep_tensor_square_decomp :
∃ (G : Type) (_ : Group G) (_ : Fintype G),
Fintype.card G = 10200960 ∧
IsSimpleGroup G ∧
∃ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V) (ρ : Representation ℂ G V),
Module.finrank ℂ V = 22 ∧
ρ.IsIrreducible ∧
(@isotypicComponents (MonoidAlgebra ℂ G) (V ⊗[ℂ] V) _ _
(Module.compHom (V ⊗[ℂ] V)
(Representation.asAlgebraHom (ρ.tprod ρ)).toRingHom)).ncard = 4 := ⊢ ∃ G x x_1,
Fintype.card G = 10200960 ∧
IsSimpleGroup G ∧
∃ V x_2 x_3 ρ,
Module.finrank ℂ V = 22 ∧ ρ.IsIrreducible ∧ (isotypicComponents (MonoidAlgebra ℂ G) (V ⊗[ℂ] V)).ncard = 4
All goals completed! 🐙
Darboux's theorem (symplectic forms are locally standard)
darboux
#92
Verso theorem preview
theorem declaration uses `sorry`darboux {n : ℕ} {U : Set (LeanEval.Geometry.Darboux.E n)} (_hU : IsOpen U)
(α : LeanEval.Geometry.Darboux.E n → LeanEval.Geometry.Darboux.E n [⋀^Fin 2]→L[ℝ] ℝ) (_hα : LeanEval.Geometry.Darboux.IsSymplecticOn α U)
{x : LeanEval.Geometry.Darboux.E n} (_hx : x ∈ U) :
∃ φ : OpenPartialHomeomorph (LeanEval.Geometry.Darboux.E n) (LeanEval.Geometry.Darboux.E n),
x ∈ φ.source ∧ φ.source ⊆ U ∧
ContDiffOn ℝ ∞ (φ : LeanEval.Geometry.Darboux.E n → LeanEval.Geometry.Darboux.E n) φ.source ∧
ContDiffOn ℝ ∞ (φ.symm : LeanEval.Geometry.Darboux.E n → LeanEval.Geometry.Darboux.E n) φ.target ∧
∀ z ∈ φ.target,
LeanEval.Geometry.Darboux.IsDarbouxNormal
((α (φ.symm z)).compContinuousLinearMap
(fderiv ℝ (φ.symm : LeanEval.Geometry.Darboux.E n → LeanEval.Geometry.Darboux.E n) z)) := n:ℕU:Set (E n)_hU:IsOpen Uα:E n → E n [⋀^Fin 2]→L[ℝ] ℝ_hα:IsSymplecticOn α Ux:E n_hx:x ∈ U⊢ ∃ φ,
x ∈ φ.source ∧
φ.source ⊆ U ∧
ContDiffOn ℝ ∞ (↑φ) φ.source ∧
ContDiffOn ℝ ∞ (↑φ.symm) φ.target ∧
∀ z ∈ φ.target, IsDarbouxNormal ((α (↑φ.symm z)).compContinuousLinearMap (fderiv ℝ (↑φ.symm) z))
All goals completed! 🐙
Ado's theorem in characteristic zero
adoCharZero
#93
Verso theorem preview
theorem declaration uses `sorry`adoCharZero [CharZero K] [FiniteDimensional K L] :
∃ (V : Type u) (_ : AddCommGroup V) (_ : Module K V) (_ : FiniteDimensional K V)
(ρ : L →ₗ⁅K⁆ Module.End K V), Function.Injective ρ := K:Type uL:Type uinst✝⁴:Field Kinst✝³:LieRing Linst✝²:LieAlgebra K Linst✝¹:CharZero Kinst✝:FiniteDimensional K L⊢ ∃ V x x_1, ∃ (_ : FiniteDimensional K V), ∃ ρ, Function.Injective ⇑ρ
All goals completed! 🐙
The Hopf Umlaufsatz (theorem of turning tangents)
hopf_umlaufsatz
#94
Verso theorem preview
theorem declaration uses `sorry`hopf_umlaufsatz {r : ℝ → LeanEval.Geometry.HopfUmlaufsatz.Plane} {α : ℝ → ℝ}
(_hr : LeanEval.Geometry.HopfUmlaufsatz.IsPositiveSimpleClosedUnitSpeedCurve r)
(_hα : LeanEval.Geometry.HopfUmlaufsatz.IsTangentAngleLift r α) :
totalCurvature α = 2 * Real.pi := r:ℝ → Planeα:ℝ → ℝ_hr:IsPositiveSimpleClosedUnitSpeedCurve r_hα:IsTangentAngleLift r α⊢ totalCurvature α = 2 * Real.pi
All goals completed! 🐙
Radó's theorem on Riemann surfaces
rado_riemannSurface
#95
Verso theorem preview
theorem declaration uses `sorry`rado_riemannSurface {X : Type*} [TopologicalSpace X] [T2Space X] [ConnectedSpace X]
[ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] :
SecondCountableTopology X := X:Type u_1inst✝⁴:TopologicalSpace Xinst✝³:T2Space Xinst✝²:ConnectedSpace Xinst✝¹:ChartedSpace ℂ Xinst✝:IsManifold (modelWithCornersSelf ℂ ℂ) 1 X⊢ SecondCountableTopology X
All goals completed! 🐙
Morrison–Walker Lemma B.0.1: adapting families of maps to open covers
families_of_maps_b01
#96
Verso theorem preview
/-- **Lemma B.0.1** of Morrison–Walker, *The Blob Complex*
(arXiv:1009.5025, §B), continuous case. -/
theorem declaration uses `sorry`continuous
{P : Set (Fin k → ℝ)} (_hP : IsPolyhedron P)
[CompactSpace X]
(U : ι → Set X) (_hUopen : ∀ α, IsOpen (U α))
(ρ : PartitionOfUnity ι X univ) (_hρ : ρ.IsSubordinate U)
(f : C(P × X, T)) :
∃ F : C(I × P × X, T),
(∀ p : P, ∀ x : X, F (0, p, x) = f (p, x)) ∧
(∃ K : Subdivision P,
∀ D ∈ K.complex.facets,
AdaptedTo U k
(fun q : closedCell P D × X => F (1, q.1.1, q.2))) ∧
(∀ S : Set X, Supported (f := f.toFun) S →
Supported (fun q : (I × P) × X => F (q.1.1, q.1.2, q.2)) S) ∧
(∀ Q : Set P, IsBoundarySubpolyhedron Q →
∀ S' : Set X,
Supported (fun q : Q × X => f (q.1.1, q.2)) S' →
Supported (fun q : (I × Q) × X => F (q.1.1, q.1.2.1, q.2)) S') := k:ℕι:Type u_1X:Type u_2T:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace TP:Set (Fin k → ℝ)_hP:IsPolyhedron Pinst✝:CompactSpace XU:ι → Set X_hUopen:∀ (α : ι), IsOpen[inst✝²] (U α)ρ:PartitionOfUnity ι X_hρ:ρ.IsSubordinate Uf:C(↑P × X, T)⊢ ∃ F,
(∀ (p : ↑P) (x : X), F (0, p, x) = f (p, x)) ∧
(∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => F (1, ↑q.1, q.2)) ∧
(∀ (S : Set X), Supported f.toFun S → Supported (fun q => F (q.1.1, q.1.2, q.2)) S) ∧
∀ (Q : Set ↑P),
IsBoundarySubpolyhedron Q →
∀ (S' : Set X), Supported (fun q => f (↑q.1, q.2)) S' → Supported (fun q => F (q.1.1, ↑q.1.2, q.2)) S'
All goals completed! 🐙/-- **Lemma B.0.1**, bi-Lipschitz variant (part 4 of the paper). -/
theorem declaration uses `sorry`biLipschitz
{X T : Type*} [MetricSpace X] [MetricSpace T] [CompactSpace X]
{P : Set (Fin k → ℝ)} (_hP : IsPolyhedron P)
{ι : Type*}
(U : ι → Set X) (_hUopen : ∀ α, IsOpen (U α))
(ρ : PartitionOfUnity ι X univ) (_hρ : ρ.IsSubordinate U)
(f : C(P × X, T))
(slice : P → (X ≃ₜ T))
(_h_slice_eq : ∀ p : P, ∀ x : X, f (p, x) = slice p x)
(L : NNReal)
(_hf_joint : LipschitzWith L f.toFun)
(_hf_slice_inv : ∀ p : P, LipschitzWith L (slice p).symm) :
∃ F : C(I × P × X, T), ∃ L' : NNReal, ∃ Slice : I × P → (X ≃ₜ T),
(∀ p : P, ∀ x : X, F (0, p, x) = f (p, x)) ∧
(∀ t : I, ∀ p : P, ∀ x : X, F (t, p, x) = Slice (t, p) x) ∧
(∃ K : Subdivision P,
∀ D ∈ K.complex.facets,
AdaptedTo U k
(fun q : closedCell P D × X => F (1, q.1.1, q.2))) ∧
(∀ S : Set X, Supported (f := f.toFun) S →
Supported (fun q : (I × P) × X => F (q.1.1, q.1.2, q.2)) S) ∧
(∀ Q : Set P, IsBoundarySubpolyhedron Q →
∀ S' : Set X,
Supported (fun q : Q × X => f (q.1.1, q.2)) S' →
Supported (fun q : (I × Q) × X => F (q.1.1, q.1.2.1, q.2)) S') ∧
(∀ tp : I × P, LipschitzWith L' (Slice tp)) ∧
(∀ tp : I × P, LipschitzWith L' (Slice tp).symm) := k:ℕX:Type u_4T:Type u_5inst✝²:MetricSpace Xinst✝¹:MetricSpace Tinst✝:CompactSpace XP:Set (Fin k → ℝ)_hP:IsPolyhedron Pι:Type u_6U:ι → Set X_hUopen:∀ (α : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U α)ρ:PartitionOfUnity ι X_hρ:ρ.IsSubordinate Uf:C(↑P × X, T)slice:↑P → X ≃ₜ T_h_slice_eq:∀ (p : ↑P) (x : X), f (p, x) = (slice p) xL:NNReal_hf_joint:LipschitzWith L f.toFun_hf_slice_inv:∀ (p : ↑P), LipschitzWith L ⇑(slice p).symm⊢ ∃ F L' Slice,
(∀ (p : ↑P) (x : X), F (0, p, x) = f (p, x)) ∧
(∀ (t : ↑I) (p : ↑P) (x : X), F (t, p, x) = (Slice (t, p)) x) ∧
(∃ K, ∀ D ∈ K.complex.facets, AdaptedTo U k fun q => F (1, ↑q.1, q.2)) ∧
(∀ (S : Set X), Supported f.toFun S → Supported (fun q => F (q.1.1, q.1.2, q.2)) S) ∧
(∀ (Q : Set ↑P),
IsBoundarySubpolyhedron Q →
∀ (S' : Set X),
Supported (fun q => f (↑q.1, q.2)) S' → Supported (fun q => F (q.1.1, ↑q.1.2, q.2)) S') ∧
(∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp)) ∧ ∀ (tp : ↑I × ↑P), LipschitzWith L' ⇑(Slice tp).symm
All goals completed! 🐙
Pick's theorem
pick
#97
Verso theorem preview
theorem declaration uses `sorry`pick {n : ℕ} (hn : 3 ≤ n) (v : Fin n → ℤ × ℤ)
(hsimple : LeanEval.Geometry.PicksTheorem.IsSimple (LeanEval.Geometry.PicksTheorem.latPoly v)) :
area ((LeanEval.Geometry.PicksTheorem.latPoly v).boundary (R := ℝ))
= (interiorPts v : ℝ) + (boundaryPts v : ℝ) / 2 - 1 := n:ℕhn:3 ≤ nv:Fin n → ℤ × ℤhsimple:IsSimple (latPoly v)⊢ area (Polygon.boundary ℝ (latPoly v)) = ↑(interiorPts v) + ↑(boundaryPts v) / 2 - 1
All goals completed! 🐙
The Golod–Shafarevich inequality
golod_shafarevich_inequality
#98
Verso theorem preview
theorem declaration uses `sorry`golod_shafarevich_inequality (p : ℕ) [Fact p.Prime] (Q : Type)
[Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
[DiscreteTopology Q] [Finite Q] :
IsPGroup p Q → Nontrivial Q →
(generatorRank Q : ℝ) ^ 2 < 4 * (relationRank p Q : ℝ) := p:ℕinst✝⁵:Fact (Nat.Prime p)Q:Typeinst✝⁴:Group Qinst✝³:TopologicalSpace Qinst✝²:IsTopologicalGroup Qinst✝¹:DiscreteTopology Qinst✝:Finite Q⊢ IsPGroup p Q → Nontrivial Q → ↑(generatorRank Q) ^ 2 < 4 * ↑(relationRank p Q)
All goals completed! 🐙
Cauchy–Kovalevskaya theorem
cauchy_kovalevskaya
#99
Verso theorem preview
theorem declaration uses `sorry`cauchy_kovalevskaya {d : ℕ}
(F : LeanEval.Analysis.E d × ℝ × ℝ → LeanEval.Analysis.E d) (f : LeanEval.Analysis.E d × ℝ × ℝ → ℝ) (u₀ : LeanEval.Analysis.E d → ℝ)
(_hF : AnalyticOnNhd ℝ F univ) (_hf : AnalyticOnNhd ℝ f univ)
(_hu₀ : AnalyticOnNhd ℝ u₀ univ) (x₀ : LeanEval.Analysis.E d) :
∃ (U : Set (LeanEval.Analysis.E d × ℝ)) (u : LeanEval.Analysis.E d × ℝ → ℝ),
(x₀, (0 : ℝ)) ∈ U ∧ IsOpen U ∧ AnalyticOnNhd ℝ u U ∧
(∀ x : LeanEval.Analysis.E d, (x, (0 : ℝ)) ∈ U → u (x, 0) = u₀ x) ∧
(∀ p ∈ U,
fderiv ℝ u p ((0 : LeanEval.Analysis.E d), (1 : ℝ)) =
fderiv ℝ u p (F (p.1, p.2, u p), (0 : ℝ)) + f (p.1, p.2, u p)) ∧
(∀ v : LeanEval.Analysis.E d × ℝ → ℝ, AnalyticOnNhd ℝ v U →
(∀ x : LeanEval.Analysis.E d, (x, (0 : ℝ)) ∈ U → v (x, 0) = u₀ x) →
(∀ p ∈ U,
fderiv ℝ v p ((0 : LeanEval.Analysis.E d), (1 : ℝ)) =
fderiv ℝ v p (F (p.1, p.2, v p), (0 : ℝ)) + f (p.1, p.2, v p)) →
∀ p ∈ U, u p = v p) := d:ℕF:E d × ℝ × ℝ → E df:E d × ℝ × ℝ → ℝu₀:E d → ℝ_hF:AnalyticOnNhd ℝ F univ_hf:AnalyticOnNhd ℝ f univ_hu₀:AnalyticOnNhd ℝ u₀ univx₀:E d⊢ ∃ U u,
(x₀, 0) ∈ U ∧
IsOpen U ∧
AnalyticOnNhd ℝ u U ∧
(∀ (x : E d), (x, 0) ∈ U → u (x, 0) = u₀ x) ∧
(∀ p ∈ U, (fderiv ℝ u p) (0, 1) = (fderiv ℝ u p) (F (p.1, p.2, u p), 0) + f (p.1, p.2, u p)) ∧
∀ (v : E d × ℝ → ℝ),
AnalyticOnNhd ℝ v U →
(∀ (x : E d), (x, 0) ∈ U → v (x, 0) = u₀ x) →
(∀ p ∈ U, (fderiv ℝ v p) (0, 1) = (fderiv ℝ v p) (F (p.1, p.2, v p), 0) + f (p.1, p.2, v p)) →
∀ p ∈ U, u p = v p
All goals completed! 🐙
Existence of a non-isotopic pair of oriented knots
exists_nonisotopic_knots
#100
Verso theorem preview
theorem declaration uses `sorry`exists_nonisotopic_knots : ∃ K₁ K₂ : LeanEval.KnotTheory.Knot, ¬ K₁.Isotopic K₂ := ⊢ ∃ K₁ K₂, ¬K₁.Isotopic K₂
All goals completed! 🐙
Moran's equality for affine-symmetric iterated function systems
moran_equality_affine
#101
Verso theorem preview
theorem declaration uses `sorry`moran_equality_affine {d n : ℕ} (hn : 1 ≤ n)
(f : Fin n → EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)) (lam : ℝ)
(h_aff : LeanEval.Dynamics.IsAffineSymmetricIFS f lam)
(h_osc : LeanEval.Dynamics.OpenSetCondition f)
{S : Set (EuclideanSpace ℝ (Fin d))} (hS : LeanEval.Dynamics.IsAttractor f S) :
dimH S = ENNReal.ofReal (- Real.log n / Real.log lam) := d:ℕn:ℕhn:1 ≤ nf:Fin n → EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)lam:ℝh_aff:IsAffineSymmetricIFS f lamh_osc:OpenSetCondition fS:Set (EuclideanSpace ℝ (Fin d))hS:IsAttractor f S⊢ dimH S = ENNReal.ofReal (-Real.log ↑n / Real.log lam)
All goals completed! 🐙
A 3-manifold group with no faithful representation into GL(4, ℝ)
nonlinear_three_manifold_group
#102
Verso theorem preview
theorem declaration uses `sorry`nonlinear_three_manifold_group :
∃ (M : LeanEval.Topology.Closed3Manifold) (x : M.carrier),
∀ f : FundamentalGroup M.carrier x →* GL (Fin 4) ℝ, ¬ Function.Injective f := ⊢ ∃ M x, ∀ (f : FundamentalGroup M.carrier x →* GL (Fin 4) ℝ), ¬Function.Injective ⇑f
All goals completed! 🐙
Jordan curve theorem
jordan_curve
#103
Verso theorem preview
theorem declaration uses `sorry`jordan_curve (r : Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 → EuclideanSpace ℝ (Fin 2))
(_hcont : Continuous r) (_hinj : Function.Injective r) :
Nat.card
(ConnectedComponents ((Set.range r)ᶜ : Set (EuclideanSpace ℝ (Fin 2)))) =
2 := r:↑(Metric.sphere 0 1) → EuclideanSpace ℝ (Fin 2)_hcont:Continuous r_hinj:Function.Injective r⊢ Nat.card (ConnectedComponents ↑(Set.range r)ᶜ) = 2
All goals completed! 🐙
Riesz brothers' theorem
riesz_brothers_theorem
#104
Lean theorem statement
/-- **Riesz brothers' theorem.** Let `μ` be a complex Borel measure on
the unit circle such that `∫ z^n dμ = 0` for every `n ≥ 1`. Then `μ` is
absolutely continuous with respect to Haar measure. The usual density
formulation follows by applying the Radon–Nikodym theorem to this conclusion;
the hypothesis transfers the Fourier-vanishing property to that density. This
corollary is not part of the formal statement here. -/
theorem riesz_brothers_theorem (μ : ComplexMeasure UnitAddCircle)
(hμ : ∀ n : ℕ, 1 ≤ n → ∫ᵛ z, fourier n z ∂[ContinuousLinearMap.mul ℝ ℂ; μ] = 0) :
μ ≪ᵥ AddCircle.haarAddCircle.toENNRealVectorMeasure := by
sorry
Gauss-Wantzel constructible regular polygon theorem
gauss_wantzel_constructible_polygon
#105
Lean theorem statement
/-- **Gauss-Wantzel constructible polygon theorem** (§174): a regular `n`-gon
is straightedge-and-compass constructible exactly for the Gauss-Wantzel
integers. -/
theorem gauss_wantzel_constructible_polygon (n : ℕ) (hn : 3 ≤ n) :
IsConstructible (Real.cos (2 * Real.pi / n)) ↔ GaussWantzelNumber n := by
sorry
No bounded projection from L^1 onto H^1
H1_not_closedComplemented
#106
Verso theorem preview
theorem declaration uses `sorry`H1_not_closedComplemented :
¬ LeanEval.Analysis.H1.ClosedComplemented := ⊢ ¬H1.ClosedComplemented
All goals completed! 🐙
Fundamental theorem of topos theory
fundamental_topos_theory
#107
Verso theorem preview
theorem declaration uses `sorry`fundamental_topos_theory {E : Type*} [Category E]
(hE : LeanEval.ToposTheory.IsTopos E) (X : E) : LeanEval.ToposTheory.IsTopos (Over X) := E:Type u_1inst✝:Category.{u_2, u_1} EhE:IsTopos EX:E⊢ IsTopos (Over X)
All goals completed! 🐙
Hurewicz theorem in degree 1 (H₁ = abelianization of π₁)
hurewicz_h1_abelianization
#108
Lean theorem statement
/-- **Hurewicz (n = 1).** For a path-connected space `X`, `H₁(X;ℤ)` is the
abelianization of `π₁(X, x)`. -/
theorem hurewicz_h1_abelianization
(X : Type) [TopologicalSpace X] [PathConnectedSpace X] (x : X) :
Nonempty (Additive (Abelianization (FundamentalGroup X x)) ≃+
(IntegralHomology 1 X : Type)) := by
sorry
Anosov–Bowen shadowing lemma
anosov_bowen_shadowing
#109
Lean theorem statement
/-- **Anosov–Bowen shadowing lemma** (Anosov 1967; Bowen 1975). Every
compact hyperbolic invariant set has the shadowing property. -/
theorem hyperbolic_has_shadowing
(T : E d ≃ₜ E d) (K : Set (E d))
(_hKc : IsCompact K) (_hK : IsHyperbolic T K) :
HasShadowing (T : E d → E d) K := by
sorry
Liouville–Arnold theorem on integrable systems
liouville_arnold
#110
Verso theorem preview
theorem declaration uses `sorry`liouville_arnold {n : ℕ} (F : Fin n → LeanEval.Geometry.LiouvilleArnold.E n → ℝ) (U : Set (LeanEval.Geometry.LiouvilleArnold.E n)) (_hU : IsOpen U)
(_hLI : LeanEval.Geometry.LiouvilleArnold.IsLiouvilleIntegrable F U)
(c : Fin n → ℝ)
(_hMc_sub : LeanEval.Geometry.LiouvilleArnold.levelSet F c ⊆ U)
(_hMc_compact : IsCompact (LeanEval.Geometry.LiouvilleArnold.levelSet F c))
(_hMc_connected : IsConnected (LeanEval.Geometry.LiouvilleArnold.levelSet F c)) :
Nonempty ((LeanEval.Geometry.LiouvilleArnold.levelSet F c) ≃ₜ (Fin n → AddCircle (1 : ℝ))) := n:ℕF:Fin n → E n → ℝU:Set (E n)_hU:IsOpen U_hLI:IsLiouvilleIntegrable F Uc:Fin n → ℝ_hMc_sub:levelSet F c ⊆ U_hMc_compact:IsCompact (levelSet F c)_hMc_connected:IsConnected (levelSet F c)⊢ Nonempty (↑(levelSet F c) ≃ₜ (Fin n → AddCircle 1))
All goals completed! 🐙
Poincaré–Siegel linearisation theorem
poincare_siegel_linearisation
#111
Lean theorem statement
/-- **Poincaré–Siegel linearisation theorem.** If `α` is Diophantine,
`λ = e^{2πiα}`, and `f` is holomorphic near `0` with `f 0 = 0` and
`f'(0) = λ`, then there is a holomorphic germ `u` with `u 0 = 0`,
`u'(0) = 1`, and `f(u z) = u(λ z)` for `z` near `0`. -/
theorem poincare_siegel
(α : ℝ) (_hα : IsDiophantine α)
(lam : ℂ) (_hlam : lam = Complex.exp (2 * Real.pi * Complex.I * (α : ℂ)))
(f : ℂ → ℂ) (_hf : AnalyticAt ℂ f 0) (_hf0 : f 0 = 0)
(_hmult : deriv f 0 = lam) :
∃ u : ℂ → ℂ, AnalyticAt ℂ u 0 ∧ u 0 = 0 ∧ deriv u 0 = 1 ∧
∀ᶠ z in nhds (0 : ℂ), f (u z) = u (lam * z) := by
sorry
General recursive equals Turing computable
turing_recursive_equiv
#112
Verso theorem preview
theorem declaration uses `sorry`turing_recursive_equiv (f : ℕ → ℕ) :
Computable f ↔ Nonempty (TM2Computable encodeNat encodeNat f) := f:ℕ → ℕ⊢ Computable f ↔ Nonempty (TM2Computable encodeNat encodeNat f)
All goals completed! 🐙
Sobolev embedding theorem (Morrey regime)
sobolev_embedding_morrey
#113
Verso theorem preview
theorem declaration uses `sorry`sobolev_embedding {n k r : ℕ} {α p : ℝ}
(_hp : (n : ℝ) < p) (_hα : 0 < α) (_hα1 : α ≤ 1)
(_hgap : (r : ℝ) + α < (k : ℝ) - n / p)
(f : LeanEval.Analysis.SobolevMorreyProblem.E n → ℝ) (_hf : LeanEval.Analysis.SobolevMorreyProblem.MemSobolevWk k (ENNReal.ofReal p) f) :
∃ g : LeanEval.Analysis.SobolevMorreyProblem.E n → ℝ, f =ᵐ[volume] g ∧ LeanEval.Analysis.SobolevMorreyProblem.MemHolder r α g := n:ℕk:ℕr:ℕα:ℝp:ℝ_hp:↑n < p_hα:0 < α_hα1:α ≤ 1_hgap:↑r + α < ↑k - ↑n / pf:E n → ℝ_hf:MemSobolevWk k (ENNReal.ofReal p) f⊢ ∃ g, f =ᵐ[volume] g ∧ LeanEval.Analysis.SobolevMorreyProblem.MemHolder r α g
All goals completed! 🐙
Wigner semicircle law
wigner_semicircle
#114
Verso theorem preview
theorem declaration uses `sorry`wigner_semicircle {Ω : Type*} [MeasurableSpace Ω]
(μ : Measure Ω) [IsProbabilityMeasure μ]
(X : ℕ → ℕ → Ω → ℝ)
(_hX_meas : ∀ i j, Measurable (X i j))
(_hX_indep : iIndepFun
(fun ij : {p : ℕ × ℕ // p.1 ≤ p.2} => X ij.val.1 ij.val.2) μ)
(_hX_iid : ∀ i j i' j', i ≤ j → i' ≤ j' →
ProbabilityTheory.IdentDistrib (X i j) (X i' j') μ μ)
(_hX_int : ∀ i j, i ≤ j → Integrable (X i j) μ)
(_hX_sq_int : ∀ i j, i ≤ j → Integrable (fun ω => (X i j ω) ^ 2) μ)
(_hX_mean : ∀ i j, i ≤ j → ∫ ω, X i j ω ∂μ = 0)
(_hX_var : ∀ i j, i ≤ j → ∫ ω, (X i j ω) ^ 2 ∂μ = 1) :
∀ᵐ ω ∂μ,
∀ (f : ℝ → ℝ), Continuous f → (∃ M, ∀ x, ‖f x‖ ≤ M) →
Tendsto
(fun n : ℕ =>
∫ x, f x ∂ (empiricalSpectralMeasureHerm
(wignerMatrix_isHermitian X n ω)).map
(fun x : ℝ => x / Real.sqrt n))
atTop (𝓝 (∫ x, f x ∂semicircleLaw)) := Ω:Type u_1inst✝¹:MeasurableSpace Ωμ:Measure Ωinst✝:IsProbabilityMeasure μX:ℕ → ℕ → Ω → ℝ_hX_meas:∀ (i j : ℕ), Measurable (X i j)_hX_indep:iIndepFun (fun ij => X (↑ij).1 (↑ij).2) μ_hX_iid:∀ (i j i' j' : ℕ), i ≤ j → i' ≤ j' → IdentDistrib (X i j) (X i' j') μ μ_hX_int:∀ (i j : ℕ), i ≤ j → Integrable (X i j) μ_hX_sq_int:∀ (i j : ℕ), i ≤ j → Integrable (fun ω => X i j ω ^ 2) μ_hX_mean:∀ (i j : ℕ), i ≤ j → ∫ (ω : Ω), X i j ω ∂μ = 0_hX_var:∀ (i j : ℕ), i ≤ j → ∫ (ω : Ω), X i j ω ^ 2 ∂μ = 1⊢ ∀ᵐ (ω : Ω) ∂μ,
∀ (f : ℝ → ℝ),
Continuous f →
(∃ M, ∀ (x : ℝ), ‖f x‖ ≤ M) →
Tendsto (fun n => ∫ (x : ℝ), f x ∂Measure.map (fun x => x / √↑n) (empiricalSpectralMeasureHerm ⋯)) atTop
(𝓝 (∫ (x : ℝ), f x ∂semicircleLaw))
All goals completed! 🐙
Ornstein–Weiss ℤᵈ Rokhlin lemma
ornstein_weiss_rokhlin
#115
Verso theorem preview
theorem declaration uses `sorry`ornstein_weiss_rokhlin {Ω : Type*} [MeasurableSpace Ω]
[StandardBorelSpace Ω]
{d : ℕ} (_hd : 1 ≤ d) (μ : Measure Ω) [IsProbabilityMeasure μ]
(T : (Fin d → ℤ) → Ω → Ω)
(_hid : ∀ x, T 0 x = x)
(_hT : ∀ v, MeasurePreserving (T v) μ μ)
(_hgrp : ∀ u v x, T (u + v) x = T u (T v x))
(_hfree : LeanEval.Dynamics.IsFreeAction μ T)
(N : ℕ) (_hN : 1 ≤ N) {ε : ENNReal} (_hε : 0 < ε) :
∃ B : Set Ω,
MeasurableSet B ∧
((boxShape d N : Finset (Fin d → ℤ)) : Set (Fin d → ℤ)).PairwiseDisjoint
(fun v => T v '' B) ∧
μ (⋃ v ∈ boxShape d N, T v '' B) ≥ 1 - ε := Ω:Type u_1inst✝²:MeasurableSpace Ωinst✝¹:StandardBorelSpace Ωd:ℕ_hd:1 ≤ dμ:Measure Ωinst✝:IsProbabilityMeasure μT:(Fin d → ℤ) → Ω → Ω_hid:∀ (x : Ω), T 0 x = x_hT:∀ (v : Fin d → ℤ), MeasurePreserving (T v) μ μ_hgrp:∀ (u v : Fin d → ℤ) (x : Ω), T (u + v) x = T u (T v x)_hfree:IsFreeAction μ TN:ℕ_hN:1 ≤ Nε:ENNReal_hε:0 < ε⊢ ∃ B, MeasurableSet B ∧ ((↑(boxShape d N)).PairwiseDisjoint fun v => T v '' B) ∧ μ (⋃ v ∈ boxShape d N, T v '' B) ≥ 1 - ε
All goals completed! 🐙
Halmos's generic weak-mixing theorem
halmos_generic_weak_mixing
#116
Verso theorem preview
theorem declaration uses `sorry`generic_weakly_mixing [StandardBorelSpace X]
(m : Measure X) [IsProbabilityMeasure m] [NullSingletonClass m] :
(∃ G : Set (LeanEval.Dynamics.HalmosGenericWeakMixingProblem.Automorphism m), IsGδ G ∧ Dense G ∧
∀ T ∈ G, LeanEval.Dynamics.HalmosGenericWeakMixingProblem.IsWeaklyMixing m T) ∧
(∀ T : LeanEval.Dynamics.HalmosGenericWeakMixingProblem.Automorphism m, LeanEval.Dynamics.HalmosGenericWeakMixingProblem.IsWeaklyMixing m T →
Ergodic (T.toEquiv : X → X) m) := X:Type u_1inst✝³:MeasurableSpace Xinst✝²:StandardBorelSpace Xm:Measure Xinst✝¹:IsProbabilityMeasure minst✝:NullSingletonClass m⊢ (∃ G, IsGδ G ∧ Dense G ∧ ∀ T ∈ G, IsWeaklyMixing m T) ∧
∀ (T : Automorphism m), IsWeaklyMixing m T → Ergodic (⇑T.toEquiv) m
All goals completed! 🐙
Kolmogorov–Arnold superposition theorem (non-universal Lorentz form)
kolmogorov_arnold_superposition
#117
Verso theorem preview
theorem declaration uses `sorry`kolmogorov_arnold (n : ℕ) (_hn : 1 ≤ n)
(f : (Fin n → ℝ) → ℝ) (_hf : ContinuousOn f (Set.Icc 0 1)) :
∃ (g : ℝ → ℝ) (φ : Fin (2 * n + 1) → Fin n → ℝ → ℝ),
Continuous g ∧ (∀ k l, Continuous (φ k l)) ∧
∀ x ∈ Set.Icc (0 : Fin n → ℝ) 1,
f x = ∑ k, g (∑ l, φ k l (x l)) := n:ℕ_hn:1 ≤ nf:(Fin n → ℝ) → ℝ_hf:ContinuousOn f (Set.Icc 0 1)⊢ ∃ g φ,
Continuous g ∧
(∀ (k : Fin (2 * n + 1)) (l : Fin n), Continuous (φ k l)) ∧ ∀ x ∈ Set.Icc 0 1, f x = ∑ k, g (∑ l, φ k l (x l))
All goals completed! 🐙
The Landsberg–Schaar relation
landsberg_schaar
#118
Verso theorem preview
theorem declaration uses `sorry`landsberg_schaar (p q : ℕ) (hp : Odd p) (hq : Odd q) :
gaussS (2 * q : ℕ) p
= Complex.exp ((Real.pi : ℂ) * Complex.I / 4) * gaussS (-(p : ℤ)) (2 * q) := p:ℕq:ℕhp:Odd phq:Odd q⊢ gaussS (↑(2 * q)) p = cexp (↑Real.pi * I / 4) * gaussS (-↑p) (2 * q)
All goals completed! 🐙
Strong Subadditivity of von Neumann Entropy
strong_subadditivity
#119
Verso theorem preview
theorem declaration uses `sorry`strong_subadditivity (M_ABC : Matrix (A × B × C) (A × B × C) ℂ) (h : M_ABC.PosSemidef) :
let M_AB : Matrix (A × B) (A × B) ℂ :=
.traceRight <| M_ABC.reindex (.symm <| .prodAssoc ..) (.symm <| .prodAssoc ..)
let M_BC : Matrix (B × C) (B × C) ℂ := M_ABC.traceLeft
let M_B : Matrix B B ℂ := M_BC.traceRight
LeanEval.Physics.entropy M_ABC + LeanEval.Physics.entropy M_B ≤ LeanEval.Physics.entropy M_AB + LeanEval.Physics.entropy M_BC := A:Type u_1B:Type u_2C:Type u_3inst✝⁸:Fintype Ainst✝⁷:Fintype Binst✝⁶:Fintype Cinst✝⁵:DecidableEq Ainst✝⁴:DecidableEq Binst✝³:DecidableEq Cinst✝²:Nonempty Ainst✝¹:Nonempty Binst✝:Nonempty CM_ABC:Matrix (A × B × C) (A × B × C) ℂh:M_ABC.PosSemidef⊢ let M_AB := ((Matrix.reindex (Equiv.prodAssoc A B C).symm (Equiv.prodAssoc A B C).symm) M_ABC).traceRight;
let M_BC := M_ABC.traceLeft;
let M_B := M_BC.traceRight;
entropy M_ABC + entropy M_B ≤ entropy M_AB + entropy M_BC
All goals completed! 🐙
Lax's approximation theorem for toral homeomorphisms
lax_approximation
#120
Lean theorem statement
/-- **Lax's approximation theorem.** Every toral dynamical system on `𝕋^d`
(`d ≥ 1`) is approximated arbitrarily well in the metric `δ` by cyclic cube
exchange transformations. -/
theorem lax_approximation {d : ℕ} (hd : 0 < d) (T : ToralDynamicalSystem d)
{ε : ℝ≥0∞} (hε : 0 < ε) :
∃ (n : ℕ) (S : VolumePreservingEquiv d),
IsCyclicCubeExchange S n ∧ deltaDist T.toVolumePreservingEquiv S < ε := by
sorry
Radon transform: Fourier-slice diagonalization and pseudo-inversion
radon_transform_inversion
#121
Verso theorem preview
theorem declaration uses `sorry`radon_can_be_diagonalized_and_pseudo_inverted :
(∀ φ : SchwartzMap (ℝ × ℝ) ℂ, ∀ θ k : ℝ,
fourier1 (fun p => radon (φ : ℝ × ℝ → ℂ) (p, θ)) k =
fourier2 (φ : ℝ × ℝ → ℂ) (k * Real.cos θ, k * Real.sin θ)) ∧
(∃ Rinv : (ℝ × ℝ → ℂ) → (ℝ × ℝ → ℂ),
∀ φ : SchwartzMap (ℝ × ℝ) ℂ,
Rinv (radon (φ : ℝ × ℝ → ℂ)) = (φ : ℝ × ℝ → ℂ)) := ⊢ (∀ (φ : SchwartzMap (ℝ × ℝ) ℂ) (θ k : ℝ),
fourier1 (fun p => radon ⇑φ (p, θ)) k = fourier2 ⇑φ (k * Real.cos θ, k * Real.sin θ)) ∧
∃ Rinv, ∀ (φ : SchwartzMap (ℝ × ℝ) ℂ), Rinv (radon ⇑φ) = ⇑φ
All goals completed! 🐙
Brun's theorem (convergence of the twin-prime reciprocal sum)
brun_constant_converges
#122
Verso theorem preview
theorem declaration uses `sorry`brun_constant_converges :
Summable twinPrimeReciprocalTerm := ⊢ Summable twinPrimeReciprocalTerm
All goals completed! 🐙
Radial symmetry for positive semilinear Poisson solutions
semilinear_poisson_radial_symmetry
#123
Verso theorem preview
theorem declaration uses `sorry`semilinear_poisson_radial_symmetry {n : ℕ} (hn : 0 < n)
{f : ℝ → ℝ} (u : EuclideanSpace ℝ (Fin n) → ℝ)
(hf_lipschitz : ∃ K : ℝ≥0, LipschitzWith K f)
(hu_c2 : ContDiffOn ℝ 2 u (closedBall 0 1))
(hu_solve : LeanEval.Analysis.PDE.SolvesSemilinearPoisson f u)
(hu_positive : ∀ x ∈ ball 0 1, 0 < u x) :
∃ v : ℝ → ℝ≥0,
StrictAntiOn v (Set.Icc (0 : ℝ) 1) ∧
∀ x ∈ closedBall 0 1, u x = v ‖x‖ := n:ℕhn:0 < nf:ℝ → ℝu:EuclideanSpace ℝ (Fin n) → ℝhf_lipschitz:∃ K, LipschitzWith K fhu_c2:ContDiffOn ℝ 2 u (closedBall 0 1)hu_solve:SolvesSemilinearPoisson f uhu_positive:∀ x ∈ ball 0 1, 0 < u x⊢ ∃ v, StrictAntiOn v (Set.Icc 0 1) ∧ ∀ x ∈ closedBall 0 1, u x = ↑(v ‖x‖)
All goals completed! 🐙
Fraser: Fourier decay for finite-field Kakeya sets is q^{-1} and sharp
fraser_kakeya_fourier_decay
#124
Verso theorem preview
theorem declaration uses `sorry`fraser_kakeya_fourier_decay_and_sharp {d : ℕ} (_hd : 2 ≤ d) {K : Set (LeanEval.Combinatorics.FraserKakeyaProblem.Space F d)} (_hK : LeanEval.Combinatorics.FraserKakeyaProblem.IsKakeya K)
(χ : AddChar F ℂ) (_hχ : χ ≠ 1) :
(∃ μ : LeanEval.Combinatorics.FraserKakeyaProblem.Space F d → ℝ, LeanEval.Combinatorics.FraserKakeyaProblem.IsProbabilityMeasureOn K μ ∧
∀ ξ : LeanEval.Combinatorics.FraserKakeyaProblem.Space F d, ξ ≠ 0 →
‖fourier χ μ ξ‖ ≤ (Fintype.card F : ℝ)⁻¹) ∧
(∀ κ : ℝ, 0 < κ → κ < 1 →
∃ Q : ℕ, ∀ (F' : Type*) [Field F'] [Fintype F'] [DecidableEq F'],
Q ≤ Fintype.card F' →
∃ K' : Set (LeanEval.Combinatorics.FraserKakeyaProblem.Space F' d), LeanEval.Combinatorics.FraserKakeyaProblem.IsKakeya K' ∧
∀ μ : LeanEval.Combinatorics.FraserKakeyaProblem.Space F' d → ℝ, LeanEval.Combinatorics.FraserKakeyaProblem.IsProbabilityMeasureOn K' μ →
∃ ξ : LeanEval.Combinatorics.FraserKakeyaProblem.Space F' d, ξ ≠ 0 ∧
κ * (Fintype.card F' : ℝ)⁻¹ ≤
‖fourier (AddChar.FiniteField.primitiveChar_to_Complex F') μ ξ‖) := F:Type u_1inst✝²:Field Finst✝¹:Fintype Finst✝:DecidableEq Fd:ℕ_hd:2 ≤ dK:Set (Space F d)_hK:IsKakeya Kχ:AddChar F ℂ_hχ:χ ≠ 1⊢ (∃ μ,
IsProbabilityMeasureOn K μ ∧
∀ (ξ : Space F d), ξ ≠ 0 → ‖LeanEval.Combinatorics.FraserKakeyaProblem.fourier χ μ ξ‖ ≤ (↑(Fintype.card F))⁻¹) ∧
∀ (κ : ℝ),
0 < κ →
κ < 1 →
∃ Q,
∀ (F' : Type u_2) [inst : Field F'] [inst_1 : Fintype F'] [DecidableEq F'],
Q ≤ Fintype.card F' →
∃ K',
IsKakeya K' ∧
∀ (μ : Space F' d → ℝ),
IsProbabilityMeasureOn K' μ →
∃ ξ,
ξ ≠ 0 ∧
κ * (↑(Fintype.card F'))⁻¹ ≤
‖LeanEval.Combinatorics.FraserKakeyaProblem.fourier
(AddChar.FiniteField.primitiveChar_to_Complex F') μ ξ‖
All goals completed! 🐙
Lidskii's inequality
lidskii_inequality
#125
Verso theorem preview
theorem declaration uses `sorry`lidskii_inequality {n : Type*} [Fintype n] [DecidableEq n]
{A B : Matrix n n ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian)
{p : ℝ} (_hp : 1 ≤ p) :
∑ j, |hA.eigenvalues₀ j - hB.eigenvalues₀ j| ^ p ≤
∑ j, |(hB.sub hA).eigenvalues₀ j| ^ p := n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℂB:Matrix n n ℂhA:A.IsHermitianhB:B.IsHermitianp:ℝ_hp:1 ≤ p⊢ ∑ j, |hA.eigenvalues₀ j - hB.eigenvalues₀ j| ^ p ≤ ∑ j, |⋯.eigenvalues₀ j| ^ p
All goals completed! 🐙
Chen theorem for Markoff graphs
dvd_card_connectedComponent_markoffGraph
#126
Verso theorem preview
theorem declaration uses `sorry`dvd_card_connectedComponent_markoffGraph {p : ℕ} (hp : Nat.Prime p) (hgt : 3 < p) :
∀ c : (LeanEval.Combinatorics.markoffGraph p).ConnectedComponent, p ∣ Nat.card c := p:ℕhp:Nat.Prime phgt:3 < p⊢ ∀ (c : (markoffGraph p).ConnectedComponent), p ∣ Nat.card ↥c
All goals completed! 🐙
Nyquist–Shannon sampling theorem
nyquist_shannon_sampling
#127
Verso theorem preview
theorem declaration uses `sorry`nyquist_shannon_sampling (f : 𝓢(ℝ, ℂ)) (hf : LeanEval.Analysis.NyquistShannon.FourierSupportedInNyquist f) :
∀ t : ℝ,
Summable (fun n : ℤ ↦ f (n : ℝ) * sinc (Real.pi * ((n : ℝ) - t))) ∧
f t =
∑' n : ℤ, f (n : ℝ) * sinc (Real.pi * ((n : ℝ) - t)) := f:𝓢(ℝ, ℂ)hf:FourierSupportedInNyquist f⊢ ∀ (t : ℝ), (Summable fun n => f ↑n * sinc (Real.pi * (↑n - t))) ∧ f t = ∑' (n : ℤ), f ↑n * sinc (Real.pi * (↑n - t))
All goals completed! 🐙
Local stable/unstable sets at a hyperbolic fixed point (set-level Hadamard–Perron)
stable_unstable_manifolds
#128
Verso theorem preview
theorem declaration uses `sorry`stable_unstable_manifolds_exist (n : ℕ) (f : LeanEval.Dynamics.StableUnstableManifoldsProblem.E n → LeanEval.Dynamics.StableUnstableManifoldsProblem.E n) (x₀ : LeanEval.Dynamics.StableUnstableManifoldsProblem.E n)
(_hf : ContDiffAt ℝ 1 f x₀)
(_hfix : f x₀ = x₀)
(_hhyp : LeanEval.Dynamics.StableUnstableManifoldsProblem.IsHyperbolicLinear (fderiv ℝ f x₀))
(_hf_inv : (fderiv ℝ f x₀).IsInvertible) :
∃ U : Set (LeanEval.Dynamics.StableUnstableManifoldsProblem.E n), IsOpen U ∧ x₀ ∈ U ∧
∃ Ws Wu : Set (LeanEval.Dynamics.StableUnstableManifoldsProblem.E n),
Ws = {x | (∀ k : ℕ, f^[k] x ∈ U) ∧
Tendsto (fun k => f^[k] x) atTop (𝓝 x₀)} ∧
Wu = {x | ∃ y : ℕ → LeanEval.Dynamics.StableUnstableManifoldsProblem.E n,
y 0 = x ∧
(∀ k : ℕ, y k ∈ U) ∧
(∀ k : ℕ, f (y (k + 1)) = y k) ∧
Tendsto y atTop (𝓝 x₀)} ∧
Ws ∩ Wu = {x₀} := n:ℕf:E n → E nx₀:E n_hf:ContDiffAt ℝ 1 f x₀_hfix:f x₀ = x₀_hhyp:IsHyperbolicLinear (fderiv ℝ f x₀)_hf_inv:(fderiv ℝ f x₀).IsInvertible⊢ ∃ U,
IsOpen U ∧
x₀ ∈ U ∧
∃ Ws Wu,
Ws = {x | (∀ (k : ℕ), f^[k] x ∈ U) ∧ Tendsto (fun k => f^[k] x) atTop (𝓝 x₀)} ∧
Wu = {x | ∃ y, y 0 = x ∧ (∀ (k : ℕ), y k ∈ U) ∧ (∀ (k : ℕ), f (y (k + 1)) = y k) ∧ Tendsto y atTop (𝓝 x₀)} ∧
Ws ∩ Wu = {x₀}
All goals completed! 🐙
Rokhlin lemma
rokhlin_lemma
#129
Lean theorem statement
/-- **Rokhlin lemma, not-necessarily-invertible forward-image form.** For every
aperiodic measure-preserving transformation `T` of a standard Borel probability
space `(Ω, μ)`, every height `n ≥ 1`, and every `ε > 0`, there is a measurable
base whose `n` forward-image floors `B, T B, …, T^{n−1} B` are pairwise
disjoint and whose union has outer measure at least `1 − ε`. No invertibility
assumption is made. -/
theorem rokhlin_lemma {Ω : Type*} [MeasurableSpace Ω]
[StandardBorelSpace Ω]
(μ : Measure Ω) [IsProbabilityMeasure μ] (T : Ω → Ω)
(_hT : MeasurePreserving T μ μ) (_hap : IsAperiodic T μ)
(n : ℕ) (_hn : 1 ≤ n) {ε : ENNReal} (_hε : 0 < ε) :
∃ B : Set Ω, IsRokhlinTower T B n ∧
μ (towerUnion T B n) ≥ 1 - ε := by
sorry
Tverberg's theorem
tverberg_theorem
#130
Lean theorem statement
/-- **Tverberg's theorem.** Any `(r-1)(d+1)+1` points in `ℝ^d` admit an
`r`-part Tverberg partition. -/
theorem tverberg_theorem (d r : ℕ) (hr : 1 ≤ r)
(f : Fin ((r - 1) * (d + 1) + 1) → Space d) :
HasTverbergPartition (r := r) f := by
sorry
Fang–Xia: tiling of the symmetric group by transpositions implies λ-transitivity
fang_xia_tiling_partition_transitive
#131
Verso theorem preview
theorem declaration uses `sorry`fang_xia_partition_transitive_of_tiling {n : ℕ} {Y : Set (Equiv.Perm (Fin n))}
(_h : LeanEval.Combinatorics.FangXiaTilingProblem.IsTiling (LeanEval.Combinatorics.FangXiaTilingProblem.transpositionsWithOne n) Y) :
∀ lam : LeanEval.Combinatorics.FangXiaTilingProblem.PartitionShape n, 0 ≤ lam.contentSum → LeanEval.Combinatorics.FangXiaTilingProblem.IsPartitionTransitive Y lam := n:ℕY:Set (Equiv.Perm (Fin n))_h:IsTiling (transpositionsWithOne n) Y⊢ ∀ (lam : PartitionShape n), 0 ≤ lam.contentSum → IsPartitionTransitive Y lam
All goals completed! 🐙
Mountain Pass Theorem (Ambrosetti–Rabinowitz 1973)
mountain_pass
#132
Verso theorem preview
theorem declaration uses `sorry`mountain_pass (f : E → ℝ) (_hf : ContDiff ℝ 1 f) (_hps : LeanEval.Analysis.MountainPassProblem.PalaisSmale f)
{a b : E} {ε r : ℝ} (_hmr : LeanEval.Analysis.MountainPassProblem.MountainRange f a b ε r) :
∃ x : E, LeanEval.Analysis.MountainPassProblem.IsCriticalPoint f x ∧
f x = mountainPassLevel f a b ∧ ε ≤ mountainPassLevel f a b := E:Type u_1inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:CompleteSpace Ef:E → ℝ_hf:ContDiff ℝ 1 f_hps:PalaisSmale fa:Eb:Eε:ℝr:ℝ_hmr:MountainRange f a b ε r⊢ ∃ x, IsCriticalPoint f x ∧ f x = mountainPassLevel f a b ∧ ε ≤ mountainPassLevel f a b
All goals completed! 🐙
Boone–Higman theorem (easy direction)
boone_higman_embedding
#133
Verso theorem preview
theorem declaration uses `sorry`boone_higman_embedding {G H K : Type*} [Group G] [Group H] [Group K]
[IsSimpleGroup H] [Group.IsFinitelyPresented K]
(f : G →* H) (hf : Function.Injective f)
(g : H →* K) (hg : Function.Injective g)
{n : ℕ} (φ : FreeGroup (Fin n) →* G)
(hsurj : Function.Surjective φ)
(hker : (MonoidHom.ker φ).IsFinitelyNormallyGenerated) :
LeanEval.GroupTheory.BooneHigmanEmbedding.WordProblemSolvable φ := G:Type u_1H:Type u_2K:Type u_3inst✝⁴:Group Ginst✝³:Group Hinst✝²:Group Kinst✝¹:IsSimpleGroup Hinst✝:Group.IsFinitelyPresented Kf:G →* Hhf:Function.Injective ⇑fg:H →* Khg:Function.Injective ⇑gn:ℕφ:FreeGroup (Fin n) →* Ghsurj:Function.Surjective ⇑φhker:φ.ker.IsFinitelyNormallyGenerated⊢ WordProblemSolvable φ
All goals completed! 🐙
Pascal's theorem
pascal
#134
Lean theorem statement
/-- **Pascal's theorem.** Six distinct points on a non-singular conic determine
three collinear intersection points `Aᵢ Bⱼ ∩ Aⱼ Bᵢ`. -/
theorem pascal
(M : Matrix (Fin 3) (Fin 3) ℝ) (hMsymm : M.IsSymm) (hMdet : M.det ≠ 0)
(a₁ a₂ a₃ b₁ b₂ b₃ : Fin 3 → ℝ)
(ha₁ : a₁ ≠ 0) (ha₂ : a₂ ≠ 0) (ha₃ : a₃ ≠ 0)
(hb₁ : b₁ ≠ 0) (hb₂ : b₂ ≠ 0) (hb₃ : b₃ ≠ 0)
(hdist : [a₁, a₂, a₃, b₁, b₂, b₃].Pairwise (fun v w => ¬ SamePoint v w))
(hA₁ : OnConic M a₁) (hA₂ : OnConic M a₂) (hA₃ : OnConic M a₃)
(hB₁ : OnConic M b₁) (hB₂ : OnConic M b₂) (hB₃ : OnConic M b₃) :
Collinear3 (meet a₁ b₂ a₂ b₁) (meet a₁ b₃ a₃ b₁) (meet a₂ b₃ a₃ b₂) := by
sorry
Choquet's representation theorem
choquet_representation_theorem
#135
Verso theorem preview
theorem declaration uses `sorry`choquet [MeasurableSpace X] [BorelSpace X]
(K : Set X) (hK_cpt : IsCompact K) (hK_cvx : Convex ℝ K)
{x : X} (hx : x ∈ K) :
∃ μ : Measure X, IsProbabilityMeasure μ ∧
μ (K.extremePoints ℝ)ᶜ = 0 ∧
x = ∫ y, y ∂μ := X:Type u_1inst✝⁴:NormedAddCommGroup Xinst✝³:NormedSpace ℝ Xinst✝²:CompleteSpace Xinst✝¹:MeasurableSpace Xinst✝:BorelSpace XK:Set XhK_cpt:IsCompact KhK_cvx:Convex ℝ Kx:Xhx:x ∈ K⊢ ∃ μ, IsProbabilityMeasure μ ∧ μ (Set.extremePoints ℝ K)ᶜ = 0 ∧ x = ∫ (y : X), y ∂μ
All goals completed! 🐙
Frobenius's theorem: the Frobenius kernel is normal
frobenius_kernel_isNormal
#136
Verso theorem preview
theorem declaration uses `sorry`frobenius_kernel_isNormal (G X : Type) [Group G] [Fintype G] [Fintype X]
[MulAction G X] [FaithfulSMul G X]
(hcard : 2 ≤ Fintype.card X)
(htrans : ∀ x y : X, ∃ g : G, g • x = y)
(hstab : ∀ x : X, MulAction.stabilizer G x ≠ ⊥)
(hfrob : ∀ g : G, g ≠ 1 → ∀ x y : X, g • x = x → g • y = y → x = y) :
∃ N : Subgroup G, N.Normal ∧
(N : Set G) = {1} ∪ {g : G | ∀ x : X, g • x ≠ x} := G:TypeX:Typeinst✝⁴:Group Ginst✝³:Fintype Ginst✝²:Fintype Xinst✝¹:MulAction G Xinst✝:FaithfulSMul G Xhcard:2 ≤ Fintype.card Xhtrans:∀ (x y : X), ∃ g, g • x = yhstab:∀ (x : X), MulAction.stabilizer G x ≠ ⊥hfrob:∀ (g : G), g ≠ 1 → ∀ (x y : X), g • x = x → g • y = y → x = y⊢ ∃ N, N.Normal ∧ ↑N = {1} ∪ {g | ∀ (x : X), g • x ≠ x}
All goals completed! 🐙
Jordan normal form
jordan_normal_form
#137
Lean theorem statement
/-- **Jordan normal form.** Over an algebraically closed field, every
endomorphism of `Kⁿ` admits a Jordan-chain basis. -/
theorem jordan_normal_form {K : Type*} [Field K] [IsAlgClosed K] (n : ℕ)
(f : Module.End K (StdSpace K n)) :
Nonempty (JordanChainBasis f) := by
sorry
Kirk's normal-structure fixed point theorem
kirk_normal_structure
#138
Verso theorem preview
theorem declaration uses `sorry`kirk_normal_structure [CompleteSpace E]
(hE_reflexive : Function.Surjective (NormedSpace.inclusionInDoubleDual ℝ E))
(K : Set E) (hK_nonempty : K.Nonempty) (hK_closed : IsClosed K)
(hK_bounded : Bornology.IsBounded K) (hK_convex : Convex ℝ K)
(hK_normal : LeanEval.Topology.KirkNormalStructure.HasNormalStructure K) (T : K → K)
(hT : LeanEval.Topology.KirkNormalStructure.IsNonexpansiveSelfMap K T) :
∃ x : K, IsFixedPt T x := E:Type u_1inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:CompleteSpace EhE_reflexive:Surjective ⇑(NormedSpace.inclusionInDoubleDual ℝ E)K:Set EhK_nonempty:K.NonemptyhK_closed:IsClosed KhK_bounded:Bornology.IsBounded KhK_convex:Convex ℝ KhK_normal:HasNormalStructure KT:↑K → ↑KhT:IsNonexpansiveSelfMap K T⊢ ∃ x, IsFixedPt T x
All goals completed! 🐙
Wiener–Lévy theorem
wiener_levy_analytic_calculus
#139
Lean theorem statement
/-- **Wiener–Lévy theorem.** If `φ` is complex-analytic on a neighbourhood of
the range of a Wiener-algebra function `f`, then the composed function
`φ ∘ f` is again in the Wiener algebra. -/
theorem wiener_levy_analytic_calculus (f : C(AddCircle T, ℂ))
(φ : ℂ → ℂ) (U : Set ℂ) (hf : InWienerAlgebra f)
(hU : IsOpen U) (hrange : range f ⊆ U)
(hφ : AnalyticOnNhd ℂ φ U) :
∃ g : C(AddCircle T, ℂ),
(∀ x, g x = φ (f x)) ∧ InWienerAlgebra g := by
sorry
The Hausdorff positivity (complete-monotonicity) criterion
hausdorff_positivity_criterion
#140
Lean theorem statement
/-- **Hausdorff positivity criterion** (Hausdorff 1921). A moment configuration
comes from a positive measure iff all its iterated backward differences are
nonnegative — i.e. the sequence is *completely monotone*: `(Δᵏa)ₙ ≥ 0` for all
`k ≤ n`. -/
theorem hausdorff_positivity {d : ℕ} (a : (Fin d → ℕ) → ℝ) :
IsPositiveMomentConfiguration a ↔ ∀ k n : Fin d → ℕ, k ≤ n → 0 ≤ diff a k n := by
sorry
The Lindemann–Weierstrass theorem
lindemann_weierstrass
#141
Lean theorem statement
/-- **Lindemann–Weierstrass theorem.** If `x₁, …, xₙ ∈ ℂ` are algebraic over `ℚ`
and ℚ-linearly independent, then `e^{x₁}, …, e^{xₙ}` are algebraically
independent over `ℚ`. -/
theorem lindemann_weierstrass {n : ℕ} (x : Fin n → ℂ)
(h_alg : ∀ i, IsAlgebraic ℚ (x i))
(h_lin : LinearIndependent ℚ x) :
AlgebraicIndependent ℚ (fun i => Complex.exp (x i)) := by
sorry
Sard's regular-value corollary
regular_value_ae
#142
Lean theorem statement
/-- **Regular value corollary (Sard).** For a smooth `f : ℝᵐ → ℝ`, almost every
`c ∈ ℝ` is a regular value. -/
theorem regular_value_ae {m : ℕ} (f : EuclideanSpace ℝ (Fin m) → ℝ)
(hf : ContDiff ℝ ∞ f) :
∀ᵐ c ∂(volume : Measure ℝ), IsRegularValue f c := by
sorry
Wiener's 1/f theorem
wiener_inverse_closed
#143
Lean theorem statement
/-- **Wiener's `1/f` theorem.** If a function on the circle belongs to the
Wiener algebra and has no zero on the circle, then its pointwise reciprocal
again belongs to the Wiener algebra. -/
theorem wiener_inverse_closed (f : C(AddCircle T, ℂ))
(hf : InWienerAlgebra f) (hzero : ∀ x, f x ≠ 0) :
∃ g : C(AddCircle T, ℂ),
(∀ x, g x = (f x)⁻¹) ∧ InWienerAlgebra g := by
sorry
Fundamental theorem of Riemannian geometry (Levi-Civita)
levi_civita_exists_unique
#144
Lean theorem statement
/-- **Fundamental theorem of Riemannian geometry** (Levi-Civita). On a
`C^∞` finite-dimensional Riemannian manifold there exists a smooth
torsion-free metric-compatible covariant derivative on `TM`, and any other
such connection agrees with it on smooth vector fields. -/
theorem levi_civita_exists_unique
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
[FiniteDimensional ℝ E] [CompleteSpace E]
{H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
{M : Type*} [TopologicalSpace M] [T2Space M] [ChartedSpace H M]
[IsManifold I ∞ M]
[RiemannianBundle (fun (x : M) ↦ TangentSpace I x)]
[IsContMDiffRiemannianBundle I ∞ E (fun (x : M) ↦ TangentSpace I x)] :
∃ cov : CovariantDerivative I E (TangentSpace I (M := M)),
(ContMDiffCovariantDerivative cov ∞ ∧
cov.torsion = 0 ∧ IsMetricCompatible cov) ∧
∀ cov' : CovariantDerivative I E (TangentSpace I (M := M)),
(ContMDiffCovariantDerivative cov' ∞ ∧
cov'.torsion = 0 ∧ IsMetricCompatible cov') →
SameOnSmooth cov cov' := by
sorry
Shannon capacity of the pentagon
shannon_capacity_pentagon
#145
Lean theorem statement
/-- **Lovász's theorem on Shannon capacity of the pentagon** (§238).
The Shannon capacity of the five-cycle is `√5`. -/
theorem shannon_capacity_pentagon :
HasShannonCapacity (SimpleGraph.cycleGraph 5) (Real.sqrt 5) := by
sorry
Frobenius determinant theorem
frobenius_group_determinant
#146
Verso theorem preview
theorem declaration uses `sorry`frobenius_group_determinant (G : Type*) [Group G] [Fintype G] [DecidableEq G] :
∃ (r : ℕ) (p : Fin r → MvPolynomial G ℂ),
r = Nat.card (ConjClasses G) ∧
(∀ j, Irreducible (p j)) ∧
(∀ i j, i ≠ j → ¬ Associated (p i) (p j)) ∧
groupDeterminant G = ∏ j, (p j) ^ (p j).totalDegree := G:Type u_1inst✝²:Group Ginst✝¹:Fintype Ginst✝:DecidableEq G⊢ ∃ r p,
r = Nat.card (ConjClasses G) ∧
(∀ (j : Fin r), Irreducible (p j)) ∧
(∀ (i j : Fin r), i ≠ j → ¬Associated (p i) (p j)) ∧ groupDeterminant G = ∏ j, p j ^ (p j).totalDegree
All goals completed! 🐙
Lindemann's theorem (e and π transcendental)
lindemann
#147
Lean theorem statement
/-- **Lindemann's theorem.** Both `e = exp 1` and `π` are transcendental over
`ℤ`. -/
theorem lindemann :
Transcendental ℤ (Real.exp 1) ∧ Transcendental ℤ Real.pi := by
sorry
Independence of the parallel postulate
parallel_postulate_independent
#148
Verso theorem preview
theorem declaration uses `sorry`parallel_postulate_independent :
(∃ (M : Type) (T : LeanEval.Geometry.TarskiAbsolute M), LeanEval.Geometry.Euclidean M T) ∧
(∃ (M : Type) (T : LeanEval.Geometry.TarskiAbsolute M), ¬ LeanEval.Geometry.Euclidean M T) := ⊢ (∃ M T, Euclidean M T) ∧ ∃ M T, ¬Euclidean M T
All goals completed! 🐙
Hausdorff moment problem: absolute-continuity criterion
hausdorff_absolute_continuity
#149
Verso theorem preview
theorem declaration uses `sorry`hausdorff_absolute_continuity {d : ℕ}
(μ : Measure (EuclideanSpace ℝ (Fin d)))
[IsProbabilityMeasure μ] (hμ : μ ((LeanEval.Analysis.HausdorffAbsoluteContinuity.cube d)ᶜ) = 0) :
LeanEval.Analysis.HausdorffAbsoluteContinuity.UniformlyAbsolutelyContinuous μ (volume.restrict (LeanEval.Analysis.HausdorffAbsoluteContinuity.cube d)) ↔
∃ C : ℝ, ∀ k n : Fin d → ℕ, k ≤ n →
diff (momentOf μ) k n ≤ C * diff (momentOf (volume.restrict (LeanEval.Analysis.HausdorffAbsoluteContinuity.cube d))) k n := d:ℕμ:Measure (EuclideanSpace ℝ (Fin d))inst✝:IsProbabilityMeasure μhμ:μ (cube d)ᶜ = 0⊢ UniformlyAbsolutelyContinuous μ (volume.restrict (cube d)) ↔
∃ C, ∀ (k n : Fin d → ℕ), k ≤ n → diff (momentOf μ) k n ≤ C * diff (momentOf (volume.restrict (cube d))) k n
All goals completed! 🐙
The Hausdorff–Hildebrandt–Schoenberg moment theorem
hausdorff_hildebrandt_schoenberg
#150
Lean theorem statement
/-- **Hausdorff–Hildebrandt–Schoenberg theorem.** A multi-indexed real sequence
is the moment sequence of a signed bounded-variation measure on the unit cube
`Iᵈ` iff its moments are Hausdorff bounded. -/
theorem hausdorff_hildebrandt_schoenberg {d : ℕ} (a : (Fin d → ℕ) → ℝ) :
IsMomentConfiguration a ↔ HausdorffBounded a := by
sorry
Hippocrates' theorem on lunes
hippocrates_lunes
#151
Verso theorem preview
theorem declaration uses `sorry`hippocrates_lunes (a b : ℝ) (ha : 0 < a) (hb : 0 < b) :
volume (LeanEval.Geometry.HippocratesLunes.horizontalLune a b) + volume (LeanEval.Geometry.HippocratesLunes.verticalLune a b) =
volume (LeanEval.Geometry.HippocratesLunes.rightTriangle a b) := a:ℝb:ℝha:0 < ahb:0 < b⊢ volume (horizontalLune a b) + volume (verticalLune a b) = volume (rightTriangle a b)
All goals completed! 🐙
Solvable extensions ↔ solvable groups (the missing converse in Abel–Ruffini)
solvable_by_radicals_converse
#152
Lean theorem statement
/-- **Solvable extensions ↔ solvable groups.** For a field `F` of
characteristic zero and a nonzero `p : F[X]`, every root of `p` in
`AlgebraicClosure F` lies in `solvableByRad F (AlgebraicClosure F)`
iff `p.Gal` is solvable. -/
theorem solvable_iff_solvableByRad (F : Type*) [Field F] [CharZero F]
(p : F[X]) (_hp : p ≠ 0) :
(∀ x : AlgebraicClosure F, aeval x p = 0 →
x ∈ solvableByRad F (AlgebraicClosure F)) ↔ Group.IsSolvable p.Gal := by
sorry
Schur-Weyl duality: S_k image equals centralizer of GL(V) image
symAction_range_eq_centralizer_glAction
#153
Verso theorem preview
theorem declaration uses `sorry`symAction_range_eq_centralizer_glAction {R : Type*} [Field R]
{M : Type*} [AddCommGroup M] [Module R M] [FiniteDimensional R M]
{k : ℕ} [Invertible (k.factorial : R)] :
Algebra.adjoin R (Set.range (LeanEval.RepresentationTheory.symAction R M k)) =
Subalgebra.centralizer R (Set.range (LeanEval.RepresentationTheory.glAction R M k)) := R:Type u_1inst✝⁴:Field RM:Type u_2inst✝³:AddCommGroup Minst✝²:Module R Minst✝¹:FiniteDimensional R Mk:ℕinst✝:Invertible ↑k.factorial⊢ Algebra.adjoin R (Set.range ⇑(symAction R M k)) = Subalgebra.centralizer R (Set.range ⇑(glAction R M k))
All goals completed! 🐙
Sturm's theorem
sturm
#154
Lean theorem statement
/-- **Sturm's theorem.** For a squarefree real polynomial `p` and an interval
`(a, b)` with `a < b` whose endpoints are not roots of `p`, the number of
distinct roots of `p` in `(a, b)` equals `σ(a) − σ(b)`. -/
theorem sturm (p : ℝ[X]) (hp : Squarefree p) {a b : ℝ} (hab : a < b)
(ha : p.eval a ≠ 0) (hb : p.eval b ≠ 0) :
((p.roots.toFinset).filter (fun x => a < x ∧ x < b)).card =
sigma p a - sigma p b := by
sorry
Riesz's rising sun lemma
rising_sun_lemma
#155
Verso theorem preview
theorem declaration uses `sorry`rising_sun_lemma {a b : ℝ} (hab : a < b) {f : ℝ → ℝ}
(hf : ContinuousOn f (Icc a b)) :
LeanEval.Analysis.RisingSun.HasRisingSunProperty a b f := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Icc a b)⊢ HasRisingSunProperty a b f
All goals completed! 🐙
Balanceable k-bounded partitions
balanceable_bounded_partitions
#156
Lean theorem statement
/--
For any `k`, the smallest `n` such that any `k`-bounded partition of `n` is
also balanceable is given by `2 * lcm(1, ..., k)`.
-/
theorem minimal_balanceable_of_bounded (k : ℕ) (hk : 0 < k) :
Minimal (fun n => 0 < n ∧ ∀ p : n.Partition, Bounded k p → Balanceable p) (2 * (Finset.Icc 1 k).lcm id) := by
sorry
Brauer–Fowler theorem
brauer_fowler
#157
Lean theorem statement
/-- **Brauer–Fowler theorem.** There is a function bounding the order
of a finite nonabelian simple group by the order of any involution
centralizer. -/
theorem brauer_fowler :
∃ f : ℕ → ℕ, ∀ (G : Type) [Group G] [Finite G],
IsSimpleGroup G → (∃ a b : G, a * b ≠ b * a) →
∀ t : G, orderOf t = 2 →
Nat.card G ≤ f (Nat.card (Subgroup.centralizer ({t} : Set G))) := by
sorry
Kakutani fixed-point theorem
kakutani_fixed_point
#158
Lean theorem statement
/-- **Kakutani fixed-point theorem.** Every upper-hemicontinuous
correspondence `F` from a nonempty compact convex `K ⊆ ℝᵈ` to itself, with
nonempty convex closed values, has a fixed point `x ∈ F x`. -/
theorem kakutani_fixed_point {d : ℕ}
{K : Set (EuclideanSpace ℝ (Fin d))}
(_hK_compact : IsCompact K) (_hK_convex : Convex ℝ K)
(_hK_nonempty : K.Nonempty)
(F : EuclideanSpace ℝ (Fin d) → Set (EuclideanSpace ℝ (Fin d)))
(_hF_uhc : IsUpperHemicontinuous F)
(_hF_nonempty : ∀ x ∈ K, (F x).Nonempty)
(_hF_convex : ∀ x ∈ K, Convex ℝ (F x))
(_hF_closed : ∀ x ∈ K, IsClosed (F x))
(_hF_maps : ∀ x ∈ K, F x ⊆ K) :
∃ x ∈ K, x ∈ F x := by
sorry
Lidskii–Last eigenvalue-perturbation theorem
lidskii_last
#159
Verso theorem preview
theorem declaration uses `sorry`lidskii_last {n : Type*} [Fintype n] [DecidableEq n]
{A B : Matrix n n ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) :
∑ j, |hA.eigenvalues₀ j - hB.eigenvalues₀ j| ≤
∑ i, ∑ j, ‖A i j - B i j‖ := n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℂB:Matrix n n ℂhA:A.IsHermitianhB:B.IsHermitian⊢ ∑ j, |hA.eigenvalues₀ j - hB.eigenvalues₀ j| ≤ ∑ i, ∑ j, ‖A i j - B i j‖
All goals completed! 🐙
A competition programming problem about permuting a permutation to be unimodal
permute_to_unimodal
#160
Lean theorem statement
/--
`minRearrange` correctly computes the smallest number of indices that need to be permuted in order to
turn `arr` into a unimodal permutation.
-/
theorem minRearrange_correct {arr : Array Nat} :
arr.Perm (1...=arr.size).toArray →
(∃ (x : Array Nat) (hx : x.Perm (1...=arr.size).toArray), Unimodal x ∧ differences (Vector.mk x (by simpa using hx.size_eq)) arr.toVector = minRearrange arr) ∧
(∀ (x : Array Nat) (hx : x.Perm (1...=arr.size).toArray), Unimodal x → minRearrange arr ≤ differences (Vector.mk x (by simpa using hx.size_eq)) arr.toVector) := by
sorry
Morley's trisector theorem
morley_theorem
#161
Verso theorem preview
theorem declaration uses `sorry`morley_theorem (A B C P Q R : LeanEval.Geometry.Morley.Plane)
(h : LeanEval.Geometry.Morley.IsMorleyConfiguration A B C P Q R) :
LeanEval.Geometry.Morley.IsEquilateralTriple P Q R := A:PlaneB:PlaneC:PlaneP:PlaneQ:PlaneR:Planeh:IsMorleyConfiguration A B C P Q R⊢ IsEquilateralTriple P Q R
All goals completed! 🐙
Nash equilibrium existence theorem
nash_equilibrium_exists
#162
Lean theorem statement
/-- **Nash equilibrium existence theorem.** Every finite `n`-player game
with nonempty finite pure-strategy sets and arbitrary real payoffs admits
at least one mixed-strategy Nash equilibrium. -/
theorem nash_equilibrium_exists {n : ℕ} {S : Fin n → Type*}
[∀ i, Fintype (S i)] [∀ i, Nonempty (S i)]
(u : Fin n → StrategyProfile n S → ℝ) :
∃ σ : ∀ i, S i → ℝ, IsNashEquilibrium u σ := by
sorry
Peano existence theorem for ODEs
peano_existence
#163
Verso theorem preview
theorem declaration uses `sorry`peano_existence {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
{f : E → E} (hf : Continuous f) (x₀ : E) :
∃ a : ℝ, 0 < a ∧ ∃ α : ℝ → E, α 0 = x₀ ∧
∀ t ∈ Ioo (-a) a, HasDerivAt α (f (α t)) t := E:Type u_1inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:FiniteDimensional ℝ Ef:E → Ehf:Continuous fx₀:E⊢ ∃ a, 0 < a ∧ ∃ α, α 0 = x₀ ∧ ∀ t ∈ Ioo (-a) a, HasDerivAt α (f (α t)) t
All goals completed! 🐙
Furstenberg–Weiss topological multiple recurrence (single-transformation form)
furstenberg_topological
#164
Lean theorem statement
/-- **Furstenberg–Weiss topological multiple recurrence** (single-
transformation form). Every homeomorphism `T` of a nonempty compact
metric space `X` has a multiply recurrent point. -/
theorem furstenberg_topological_recurrence {X : Type*} [MetricSpace X]
[CompactSpace X] [Nonempty X] (T : X ≃ₜ X) :
∃ x : X, IsMultiplyRecurrent (T : X → X) x := by
sorry
Baer–Suzuki theorem
baer_suzuki
#165
Verso theorem preview
theorem declaration uses `sorry`baer_suzuki {G : Type*} [Group G] [Finite G]
{p : ℕ} [Fact p.Prime] (x : G) :
x ∈ LeanEval.GroupTheory.Defs.pCore p G ↔
∀ g : G, IsPGroup p
(Subgroup.closure ({x, g * x * g⁻¹} : Set G)) := G:Type u_1inst✝²:Group Ginst✝¹:Finite Gp:ℕinst✝:Fact (Nat.Prime p)x:G⊢ x ∈ pCore p G ↔ ∀ (g : G), IsPGroup p ↥(Subgroup.closure {x, g * x * g⁻¹})
All goals completed! 🐙
Sard's theorem (critical-set image has measure zero)
sard_theorem
#166
Verso theorem preview
theorem declaration uses `sorry`sard {m n : ℕ} (f : LeanEval.Geometry.SardTheoremProblem.E m → LeanEval.Geometry.SardTheoremProblem.E n) (_hf : ContDiff ℝ ∞ f) :
volume (LeanEval.Geometry.SardTheoremProblem.criticalValues f) = 0 := m:ℕn:ℕf:E m → E n_hf:ContDiff ℝ ∞ f⊢ volume (criticalValues f) = 0
All goals completed! 🐙
Complete reducibility for compact groups
compact_group_semisimple
#167
Verso theorem preview
theorem declaration uses `sorry`compact_group_semisimple {G V : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
[NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V]
(ρ : Representation ℝ G V)
(hρ : Continuous fun p : G × V => ρ p.1 p.2) :
ρ.IsSemisimpleRepresentation := G:Type u_1V:Type u_2inst✝⁶:Group Ginst✝⁵:TopologicalSpace Ginst✝⁴:IsTopologicalGroup Ginst✝³:CompactSpace Ginst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:FiniteDimensional ℝ Vρ:Representation ℝ G Vhρ:Continuous fun p => (ρ p.1) p.2⊢ ρ.IsSemisimpleRepresentation
All goals completed! 🐙
Monge–Kantorovich existence theorem
monge_kantorovich
#168
Verso theorem preview
theorem declaration uses `sorry`monge_kantorovich_exists {X Y : Type*}
[TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X]
[TopologicalSpace Y] [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y]
(P : Measure X) (Q : Measure Y)
[IsProbabilityMeasure P] [IsProbabilityMeasure Q]
(c : X × Y → ENNReal) (_hc : Continuous c) :
∃ π ∈ LeanEval.Analysis.Couplings P Q,
∀ π' ∈ LeanEval.Analysis.Couplings P Q, kantorovichCost c π ≤ kantorovichCost c π' := X:Type u_1Y:Type u_2inst✝⁹:TopologicalSpace Xinst✝⁸:PolishSpace Xinst✝⁷:MeasurableSpace Xinst✝⁶:BorelSpace Xinst✝⁵:TopologicalSpace Yinst✝⁴:PolishSpace Yinst✝³:MeasurableSpace Yinst✝²:BorelSpace YP:Measure XQ:Measure Yinst✝¹:IsProbabilityMeasure Pinst✝:IsProbabilityMeasure Qc:X × Y → ENNReal_hc:Continuous c⊢ ∃ π ∈ Couplings P Q, ∀ π' ∈ Couplings P Q, kantorovichCost c π ≤ kantorovichCost c π'
All goals completed! 🐙
Normal spectral theorem
normal_spectral_theorem
#169
Verso theorem preview
theorem declaration uses `sorry`normal_spectral_theorem (A : Matrix n n ℂ) :
IsStarNormal A ↔
∃ U ∈ unitary (Matrix n n ℂ), ∃ d : n → ℂ,
A = U * diagonal d * star U := n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℂ⊢ IsStarNormal A ↔ ∃ U ∈ unitary (Matrix n n ℂ), ∃ d, A = U * diagonal d * star U
All goals completed! 🐙
Schauder fixed-point theorem
schauder_fixed_point
#170
Verso theorem preview
theorem declaration uses `sorry`schauder_fixed_point {E : Type*}
[NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
{K : Set E}
(_hK_compact : IsCompact K) (_hK_convex : Convex ℝ K)
(_hK_nonempty : K.Nonempty)
(f : E → E)
(_hf_cont : ContinuousOn f K) (_hf_maps : Set.MapsTo f K K) :
∃ x ∈ K, f x = x := E:Type u_1inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:CompleteSpace EK:Set E_hK_compact:IsCompact K_hK_convex:Convex ℝ K_hK_nonempty:K.Nonemptyf:E → E_hf_cont:ContinuousOn f K_hf_maps:Set.MapsTo f K K⊢ ∃ x ∈ K, f x = x
All goals completed! 🐙
Burnside p^a q^b theorem
finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow
#171
Verso theorem preview
theorem declaration uses `sorry`finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow {G : Type*} [Group G] [Fintype G]
{p q a b : ℕ}
(hp : Nat.Prime p)
(hq : Nat.Prime q)
(hpq : p ≠ q)
(hcard : Fintype.card G = p ^ a * q ^ b) :
Group.IsSolvable G := G:Type u_1inst✝¹:Group Ginst✝:Fintype Gp:ℕq:ℕa:ℕb:ℕhp:Nat.Prime phq:Nat.Prime qhpq:p ≠ qhcard:Fintype.card G = p ^ a * q ^ b⊢ Group.IsSolvable G
All goals completed! 🐙
Existence of a non-isotopic pair of oriented two-component links
exists_nonisotopic_link
#172
Verso theorem preview
theorem declaration uses `sorry`exists_nonisotopic_link : ∃ L₁ L₂ : LeanEval.KnotTheory.TwoLink, ¬ L₁.Isotopic L₂ := ⊢ ∃ L₁ L₂, ¬L₁.Isotopic L₂
All goals completed! 🐙
Pointwise and Cesàro convergence of Fourier series (Dirichlet, Fejér)
fourier_dirichlet_fejer
#173
Verso theorem preview
/-- **Dirichlet's pointwise convergence theorem** (§46). For every `C¹`
2π-periodic complex function `f`, the symmetric Fourier partial sums `S_N(f)(x)`
converge to `f(x)` at every point `x ∈ ℝ`. -/
theorem declaration uses `sorry`dirichlet_pointwise
{f : ℝ → ℂ} (_hperiod : Function.Periodic f (2 * Real.pi)) (_hC1 : ContDiff ℝ 1 f)
(x : ℝ) :
Tendsto (fun N : ℕ => fourierPartialSum f N x) atTop (𝓝 (f x)) := f:ℝ → ℂ_hperiod:Function.Periodic f (2 * Real.pi)_hC1:ContDiff ℝ 1 fx:ℝ⊢ Tendsto (fun N => fourierPartialSum f N x) atTop (𝓝 (f x))
All goals completed! 🐙/-- **Fejér's theorem** (§46). For every *continuous* 2π-periodic complex
function `f` — without the `C¹` hypothesis of Dirichlet's theorem — the Cesàro
means `σ_N(f)` of the symmetric Fourier partial sums converge to `f` uniformly
on `ℝ`. -/
theorem declaration uses `sorry`fejer
{f : ℝ → ℂ} (_hperiod : Function.Periodic f (2 * Real.pi)) (_hcont : Continuous f) :
TendstoUniformly (fun N : ℕ => fourierCesaroMean f N) f atTop := f:ℝ → ℂ_hperiod:Function.Periodic f (2 * Real.pi)_hcont:Continuous f⊢ TendstoUniformly (fun N => fourierCesaroMean f N) f atTop
All goals completed! 🐙
Schur-Weyl duality: GL(V) image equals centralizer of S_k image
glAction_range_eq_centralizer_symAction
#174
Verso theorem preview
theorem declaration uses `sorry`glAction_range_eq_centralizer_symAction {R : Type*} [Field R]
{M : Type*} [AddCommGroup M] [Module R M] [FiniteDimensional R M]
{k : ℕ} [Invertible (k.factorial : R)] :
Algebra.adjoin R (Set.range (LeanEval.RepresentationTheory.glAction R M k)) =
Subalgebra.centralizer R (Set.range (LeanEval.RepresentationTheory.symAction R M k)) := R:Type u_1inst✝⁴:Field RM:Type u_2inst✝³:AddCommGroup Minst✝²:Module R Minst✝¹:FiniteDimensional R Mk:ℕinst✝:Invertible ↑k.factorial⊢ Algebra.adjoin R (Set.range ⇑(glAction R M k)) = Subalgebra.centralizer R (Set.range ⇑(symAction R M k))
All goals completed! 🐙
Runge's theorem
runge_theorem
#175
Verso theorem preview
theorem declaration uses `sorry`runge (K : Set ℂ) (_hK : IsCompact K) (U : Set ℂ) (_hU : IsOpen U)
(_hKU : K ⊆ U) (f : ℂ → ℂ) (_hf : AnalyticOnNhd ℂ f U)
(ε : ℝ) (_hε : 0 < ε) :
∃ p q : ℂ[X], (∀ z ∈ K, q.eval z ≠ 0) ∧
(∀ z ∈ K, ‖f z - p.eval z / q.eval z‖ < ε) := K:Set ℂ_hK:IsCompact KU:Set ℂ_hU:IsOpen U_hKU:K ⊆ Uf:ℂ → ℂ_hf:AnalyticOnNhd ℂ f Uε:ℝ_hε:0 < ε⊢ ∃ p q, (∀ z ∈ K, Polynomial.eval z q ≠ 0) ∧ ∀ z ∈ K, ‖f z - Polynomial.eval z p / Polynomial.eval z q‖ < ε
All goals completed! 🐙
Kuznetsov's theorem: finitely presented simple groups have solvable word problem
boone_higman_simple
#176
Verso theorem preview
theorem declaration uses `sorry`boone_higman_simple {G : Type*} [Group G] [IsSimpleGroup G]
{n : ℕ} (φ : FreeGroup (Fin n) →* G)
(_hsurj : Function.Surjective φ)
(_hker : (MonoidHom.ker φ).IsFinitelyNormallyGenerated) :
LeanEval.GroupTheory.BooneHigmanSimpleProblem.WordProblemSolvable φ := G:Type u_1inst✝¹:Group Ginst✝:IsSimpleGroup Gn:ℕφ:FreeGroup (Fin n) →* G_hsurj:Function.Surjective ⇑φ_hker:φ.ker.IsFinitelyNormallyGenerated⊢ WordProblemSolvable φ
All goals completed! 🐙
Euler–Lagrange equation
euler_lagrange_equation
#177
Verso theorem preview
theorem declaration uses `sorry`euler_lagrange_equation {a b : ℝ} (L : ℝ → ℝ → ℝ → ℝ) (x : ℝ → ℝ) (_hab : a < b)
(_hL : ContDiff ℝ 2 (fun p : ℝ × ℝ × ℝ => L p.1 p.2.1 p.2.2))
(_hx : ContDiff ℝ 2 x)
(_hxe : LeanEval.Analysis.IsVariationalExtremum a b L x) :
∀ t ∈ Set.Ioo a b,
lagrangianPartialX L x t = deriv (lagrangianPartialV L x) t := a:ℝb:ℝL:ℝ → ℝ → ℝ → ℝx:ℝ → ℝ_hab:a < b_hL:ContDiff ℝ 2 fun p => L p.1 p.2.1 p.2.2_hx:ContDiff ℝ 2 x_hxe:IsVariationalExtremum a b L x⊢ ∀ t ∈ Ioo a b, lagrangianPartialX L x t = deriv (lagrangianPartialV L x) t
All goals completed! 🐙
Bauer's uniqueness at extreme points
bauer_extreme_point_uniqueness
#178
Verso theorem preview
theorem declaration uses `sorry`bauer_unique [MeasurableSpace X] [BorelSpace X]
(K : Set X) (hK_cpt : IsCompact K) (hK_cvx : Convex ℝ K)
{x : X} (hx : x ∈ K.extremePoints ℝ)
(μ : Measure X) [IsProbabilityMeasure μ]
(hμ : μ Kᶜ = 0) (hbar : x = ∫ y, y ∂μ) :
μ = Measure.dirac x := X:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ Xinst✝³:CompleteSpace Xinst✝²:MeasurableSpace Xinst✝¹:BorelSpace XK:Set XhK_cpt:IsCompact KhK_cvx:Convex ℝ Kx:Xhx:x ∈ Set.extremePoints ℝ Kμ:Measure Xinst✝:IsProbabilityMeasure μhμ:μ Kᶜ = 0hbar:x = ∫ (y : X), y ∂μ⊢ μ = Measure.dirac x
All goals completed! 🐙
Trace Cayley-Hamilton / Newton identity
trace_cayley_hamilton_newton
#179
Verso theorem preview
theorem declaration uses `sorry`trace_cayley_hamilton_newton {R : Type*} [CommRing R]
(A : Matrix n n R) {k : ℕ} (hk : 1 ≤ k) :
(k : R) * charpolyDescendingCoeff A k +
∑ j ∈ Finset.Icc 1 k,
trace (A ^ j) * charpolyDescendingCoeff A (k - j) = 0 := n:Type u_1inst✝²:Fintype ninst✝¹:DecidableEq nR:Type u_2inst✝:CommRing RA:Matrix n n Rk:ℕhk:1 ≤ k⊢ ↑k * charpolyDescendingCoeff A k + ∑ j ∈ Finset.Icc 1 k, (A ^ j).trace * charpolyDescendingCoeff A (k - j) = 0
All goals completed! 🐙
von Neumann double commutant theorem
vonNeumann_doubleCommutant_tfae
#180
Verso theorem preview
theorem declaration uses `sorry`vonNeumann_doubleCommutant_tfae {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
(S : StarSubalgebra ℂ (H →L[ℂ] H)) :
List.TFAE
[ Set.centralizer (Set.centralizer (S : Set (H →L[ℂ] H))) = S
, IsClosed
(ContinuousLinearMapWOT.ofCLM '' (S : Set (H →L[ℂ] H)))
, IsClosed
(ContinuousLinearMap.toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) H H ''
(S : Set (H →L[ℂ] H))) ] := H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HS:StarSubalgebra ℂ (H →L[ℂ] H)⊢ [(↑S).centralizer.centralizer = ↑S, IsClosed (ContinuousLinearMapWOT.ofCLM '' ↑S),
IsClosed (⇑(ContinuousLinearMap.toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) H H) '' ↑S)].TFAE
All goals completed! 🐙
Abel–Ruffini theorem
abel_ruffini
#181
Verso theorem preview
theorem declaration uses `sorry`abel_ruffini (n : ℕ) (_hn : 1 ≤ n) :
(∀ p : ℚ[X], p.natDegree = n → ∀ x : ℂ, aeval x p = 0 →
x ∈ solvableByRad ℚ ℂ) ↔ n ≤ 4 := n:ℕ_hn:1 ≤ n⊢ (∀ (p : ℚ[X]), p.natDegree = n → ∀ (x : ℂ), (aeval x) p = 0 → x ∈ solvableByRad ℚ ℂ) ↔ n ≤ 4
All goals completed! 🐙
Brouwer fixed-point theorem
brouwer_fixed_point
#182
Verso theorem preview
theorem declaration uses `sorry`brouwer_fixed_point {d : ℕ}
{K : Set (EuclideanSpace ℝ (Fin d))}
(_hK_compact : IsCompact K) (_hK_convex : Convex ℝ K)
(_hK_nonempty : K.Nonempty)
(f : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d))
(_hf_cont : ContinuousOn f K) (_hf_maps : MapsTo f K K) :
∃ x ∈ K, f x = x := d:ℕK:Set (EuclideanSpace ℝ (Fin d))_hK_compact:IsCompact K_hK_convex:Convex ℝ K_hK_nonempty:K.Nonemptyf:EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)_hf_cont:ContinuousOn f K_hf_maps:MapsTo f K K⊢ ∃ x ∈ K, f x = x
All goals completed! 🐙
Bing's house with two rooms is contractible
contractibleSpace_houseWithTwoRooms
#183
Verso theorem preview
theorem declaration uses `sorry`contractibleSpace_houseWithTwoRooms : ContractibleSpace LeanEval.Topology.HouseWithTwoRooms := ⊢ ContractibleSpace ↑HouseWithTwoRooms
All goals completed! 🐙
Wiener's atom-detection formula
wiener_atom_detection
#184
Verso theorem preview
theorem declaration uses `sorry`wiener_atom_detection (μ : Measure (AddCircle (2 * Real.pi))) [IsProbabilityMeasure μ] :
Tendsto
(fun N : ℕ =>
(1 / (N : ℝ)) *
∑ k ∈ Finset.Icc (1 : ℤ) N, ‖fourierCoeffMeasure μ k‖ ^ 2)
atTop
(𝓝 (∑' x : AddCircle (2 * Real.pi), ((μ {x}).toReal) ^ 2)) := μ:Measure (AddCircle (2 * π))inst✝:IsProbabilityMeasure μ⊢ Tendsto (fun N => 1 / ↑N * ∑ k ∈ Finset.Icc 1 ↑N, ‖fourierCoeffMeasure μ k‖ ^ 2) atTop
(𝓝 (∑' (x : AddCircle (2 * π)), (μ {x}).toReal ^ 2))
All goals completed! 🐙
Linear ODE with negative-real-part eigenvalues is asymptotically stable
linear_ode_asymptotic_stability
#185
Verso theorem preview
theorem declaration uses `sorry`linear_ode_asymptotic_stability (n : ℕ) (A : Matrix (Fin n) (Fin n) ℝ)
(hA : ∀ μ : ℂ,
Module.End.HasEigenvalue
(Matrix.toLin' (A.map (algebraMap ℝ ℂ))) μ → μ.re < 0)
(x : ℝ → (Fin n → ℝ))
(hx : ∀ t : ℝ, 0 < t → HasDerivAt x (A.mulVec (x t)) t) :
Filter.Tendsto (fun t : ℝ => ‖x t‖) Filter.atTop (nhds 0) := n:ℕA:Matrix (Fin n) (Fin n) ℝhA:∀ (μ : ℂ), Module.End.HasEigenvalue (Matrix.toLin' (A.map ⇑(algebraMap ℝ ℂ))) μ → μ.re < 0x:ℝ → Fin n → ℝhx:∀ (t : ℝ), 0 < t → HasDerivAt x (A *ᵥ x t) t⊢ Filter.Tendsto (fun t => ‖x t‖) Filter.atTop (nhds 0)
All goals completed! 🐙
Real cyclotomic integer with house at most 2
cyclotomic_integer_house_le_two
#186
Verso theorem preview
theorem declaration uses `sorry`cyclotomic_integer_house_le_two {K : Type*} [Field K] [NumberField K] [Algebra ℚ K]
(n : ℕ) [NeZero n] [IsCyclotomicExtension {n} ℚ K] {β : K}
(hβ_int : IsIntegral ℤ β)
(hβ_real : β ∈ NumberField.maximalRealSubfield K) :
house β ≤ 2 →
house β = 2 ∨ ∃ m : ℕ, 0 < m ∧ house β = 2 * Real.cos (Real.pi / m) := K:Type u_1inst✝⁴:Field Kinst✝³:NumberField Kinst✝²:Algebra ℚ Kn:ℕinst✝¹:NeZero ninst✝:IsCyclotomicExtension {n} ℚ Kβ:Khβ_int:IsIntegral ℤ βhβ_real:β ∈ maximalRealSubfield K⊢ house β ≤ 2 → house β = 2 ∨ ∃ m, 0 < m ∧ house β = 2 * Real.cos (Real.pi / ↑m)
All goals completed! 🐙
Koszul formula
koszul_formula
#187
Verso theorem preview
theorem declaration uses `sorry`koszul_formula {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
[FiniteDimensional ℝ E] [CompleteSpace E]
{H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
{M : Type*} [TopologicalSpace M] [ChartedSpace H M]
[IsManifold I ∞ M]
[RiemannianBundle (fun (x : M) ↦ TangentSpace I x)]
[IsContMDiffRiemannianBundle I ∞ E (fun (x : M) ↦ TangentSpace I x)]
(cov : CovariantDerivative I E (TangentSpace I (M := M)))
[ContMDiffCovariantDerivative cov ∞]
(_htor : cov.torsion = 0) (_hmet : LeanEval.Geometry.KoszulFormula.IsMetricCompatible cov)
(X Y Z : Π x : M, TangentSpace I x)
(_hX : CMDiff ∞ (T% X)) (_hY : CMDiff ∞ (T% Y)) (_hZ : CMDiff ∞ (T% Z))
(x : M) :
2 * inner ℝ (cov Y x (X x)) (Z x) =
mvfderiv I (fun y : M => inner ℝ (Y y) (Z y)) x (X x)
+ mvfderiv I (fun y : M => inner ℝ (X y) (Z y)) x (Y x)
- mvfderiv I (fun y : M => inner ℝ (X y) (Y y)) x (Z x)
- inner ℝ (X x) (mlieBracket I Y Z x)
- inner ℝ (Y x) (mlieBracket I X Z x)
+ inner ℝ (Z x) (mlieBracket I X Y x) := E:Type u_1inst✝¹⁰:NormedAddCommGroup Einst✝⁹:NormedSpace ℝ Einst✝⁸:FiniteDimensional ℝ Einst✝⁷:CompleteSpace EH:Type u_2inst✝⁶:TopologicalSpace HI:ModelWithCorners ℝ E HM:Type u_3inst✝⁵:TopologicalSpace Minst✝⁴:ChartedSpace H Minst✝³:IsManifold I ∞ Minst✝²:RiemannianBundle fun x => TangentSpace I xinst✝¹:IsContMDiffRiemannianBundle I ∞ E fun x => TangentSpace I xcov:CovariantDerivative I E (TangentSpace I)inst✝:cov.ContMDiffCovariantDerivative ∞_htor:cov.torsion = 0_hmet:LeanEval.Geometry.KoszulFormula.IsMetricCompatible covX:(x : M) → TangentSpace I xY:(x : M) → TangentSpace I xZ:(x : M) → TangentSpace I x_hX:ContMDiff I I.tangent ∞ fun x => ⟨x, X x⟩_hY:ContMDiff I I.tangent ∞ fun x => ⟨x, Y x⟩_hZ:ContMDiff I I.tangent ∞ fun x => ⟨x, Z x⟩x:M⊢ 2 * Inner.inner ℝ ((↑cov Y x) (X x)) (Z x) =
((d% fun y => Inner.inner ℝ (Y y) (Z y)) x) (X x) + ((d% fun y => Inner.inner ℝ (X y) (Z y)) x) (Y x) -
((d% fun y => Inner.inner ℝ (X y) (Y y)) x) (Z x) -
Inner.inner ℝ (X x) (mlieBracket I Y Z x) -
Inner.inner ℝ (Y x) (mlieBracket I X Z x) +
Inner.inner ℝ (Z x) (mlieBracket I X Y x)
All goals completed! 🐙
Perron-Frobenius for irreducible nonnegative matrices
irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius
#188
Verso theorem preview
theorem declaration uses `sorry`irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius {n : Type*} [Fintype n] [DecidableEq n] [Nonempty n]
(A : Matrix n n ℝ)
(hA : A.IsIrreducible) :
∃ v : n → ℝ,
Module.End.HasEigenvector (Matrix.toLin' A) (spectralRadius ℝ A).toReal v ∧
(∀ i, 0 < v i) := n:Type u_1inst✝²:Fintype ninst✝¹:DecidableEq ninst✝:Nonempty nA:Matrix n n ℝhA:A.IsIrreducible⊢ ∃ v, Module.End.HasEigenvector (Matrix.toLin' A) (spectralRadius ℝ A).toReal v ∧ ∀ (i : n), 0 < v i
All goals completed! 🐙
Rouche theorem via zero counting
rouche_zero_count_eq
#189
Verso theorem preview
theorem declaration uses `sorry`rouche_zero_count_eq {f g : ℂ → ℂ} {R : ℝ}
(hR : 0 < R)
(hf : MeromorphicNFOn f Set.univ)
(hg : AnalyticOn ℂ g Set.univ)
(hbound : ∀ z : ℂ, ‖z‖ = R → ‖g z‖ < ‖f z‖) :
(∑ᶠ z, ((divisor (f + g) (Metric.closedBall 0 R))⁺) z) =
(∑ᶠ z, ((divisor f (Metric.closedBall 0 R))⁺) z) := f:ℂ → ℂg:ℂ → ℂR:ℝhR:0 < Rhf:MeromorphicNFOn f Set.univhg:AnalyticOn ℂ g Set.univhbound:∀ (z : ℂ), ‖z‖ = R → ‖g z‖ < ‖f z‖⊢ ∑ᶠ (z : ℂ), (divisor (f + g) (Metric.closedBall 0 R))⁺ z = ∑ᶠ (z : ℂ), (divisor f (Metric.closedBall 0 R))⁺ z
All goals completed! 🐙
Complementary polynomial on the unit circle
exists_complementary_polynomial_on_unit_circle
#190
Verso theorem preview
theorem declaration uses `sorry`exists_complementary_polynomial_on_unit_circle (P : ℂ[X])
(hP : ∀ z : Circle, ‖P.eval (z : ℂ)‖ ≤ 1) :
∃ Q : ℂ[X],
Q.natDegree ≤ P.natDegree ∧
∀ z : Circle, ‖P.eval (z : ℂ)‖ ^ 2 + ‖Q.eval (z : ℂ)‖ ^ 2 = 1 := P:ℂ[X]hP:∀ (z : Circle), ‖eval (↑z) P‖ ≤ 1⊢ ∃ Q, Q.natDegree ≤ P.natDegree ∧ ∀ (z : Circle), ‖eval (↑z) P‖ ^ 2 + ‖eval (↑z) Q‖ ^ 2 = 1
All goals completed! 🐙
Bourbaki's locally convex extension of Banach–Alaoglu
banach_alaoglu_bourbaki
#191
Verso theorem preview
theorem declaration uses `sorry`banach_alaoglu_bourbaki (E : Type*) [AddCommGroup E] [Module ℝ E]
[TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E]
[LocallyConvexSpace ℝ E] (U : Set E) (_hU : U ∈ 𝓝 (0 : E)) :
IsCompact (LeanEval.Analysis.weakStarPolar E U) := E:Type u_1inst✝⁵:AddCommGroup Einst✝⁴:Module ℝ Einst✝³:TopologicalSpace Einst✝²:ContinuousAdd Einst✝¹:ContinuousSMul ℝ Einst✝:LocallyConvexSpace ℝ EU:Set E_hU:U ∈ 𝓝 0⊢ IsCompact (weakStarPolar E U)
All goals completed! 🐙
Linear programming: maximum principle and vertex optimality
lp_maximum_principle
#192
Verso theorem preview
/-- **Maximum principle for linear programming** (§101). A local maximiser of
the LP objective on the feasible region is automatically a global maximiser; and
whenever the objective is non-constant (`c ≠ 0`), the maximiser lies on the
topological frontier of the feasible region. -/
theorem declaration uses `sorry`lp_maximum_principle {m n : ℕ} (lp : LinearProgram m n)
(x : Fin m → ℝ) (_hx : x ∈ lp.feasible)
(_hlocal : IsLocalMaxOn lp.objective lp.feasible x) :
IsMaxOn lp.objective lp.feasible x ∧
(lp.c ≠ 0 → x ∈ frontier lp.feasible) := m:ℕn:ℕlp:LinearProgram m nx:Fin m → ℝ_hx:x ∈ lp.feasible_hlocal:IsLocalMaxOn lp.objective lp.feasible x⊢ IsMaxOn lp.objective lp.feasible x ∧ (lp.c ≠ 0 → x ∈ frontier lp.feasible)
All goals completed! 🐙/-- **Vertex optimality** (§101; the existence content of Dantzig's 1947 simplex
algorithm). Every linear program with a nonempty bounded feasible region admits a
global maximiser that is an extreme point (vertex) of the feasible region. -/
theorem declaration uses `sorry`simplex_algorithm {m n : ℕ} (lp : LinearProgram m n)
(_hfeas : lp.feasible.Nonempty) (_hbdd : Bornology.IsBounded lp.feasible) :
∃ x ∈ lp.feasible, IsMaxOn lp.objective lp.feasible x ∧
x ∈ Set.extremePoints ℝ lp.feasible := m:ℕn:ℕlp:LinearProgram m n_hfeas:lp.feasible.Nonempty_hbdd:Bornology.IsBounded lp.feasible⊢ ∃ x ∈ lp.feasible, IsMaxOn lp.objective lp.feasible x ∧ x ∈ Set.extremePoints ℝ lp.feasible
All goals completed! 🐙
Pell solutions are convergents of √d
pell_solution_convergent
#193
Verso theorem preview
theorem declaration uses `sorry`pell_solution_is_convergent (d : ℤ) (_hd : Squarefree d) (_hd0 : 0 < d)
(x y : ℤ) (_hx : 0 < x) (_hy : 0 < y)
(_hsol : x ^ 2 - d * y ^ 2 = 1) :
∃ n : ℕ, (GenContFract.of (Real.sqrt (d : ℝ))).convs n = (x : ℝ) / (y : ℝ) := d:ℤ_hd:Squarefree d_hd0:0 < dx:ℤy:ℤ_hx:0 < x_hy:0 < y_hsol:x ^ 2 - d * y ^ 2 = 1⊢ ∃ n, (GenContFract.of √↑d).convs n = ↑x / ↑y
All goals completed! 🐙
Symplectic matrices have determinant 1
symplectic_matrix_det
#194
Verso theorem preview
theorem declaration uses `sorry`symplectic_matrix_det {l R : Type*} [DecidableEq l] [Fintype l] [CommRing R]
{A : Matrix (l ⊕ l) (l ⊕ l) R} (_hA : A ∈ Matrix.symplecticGroup l R) :
A.det = 1 := l:Type u_1R:Type u_2inst✝²:DecidableEq linst✝¹:Fintype linst✝:CommRing RA:Matrix (l ⊕ l) (l ⊕ l) R_hA:A ∈ symplecticGroup l R⊢ A.det = 1
All goals completed! 🐙
Gaussian heat kernel solves the 1D heat equation
heat_kernel_solves_heat_equation
#195
Verso theorem preview
theorem declaration uses `sorry`heat_kernel_solves_heat_equation (f : ℝ → ℝ) (hf_cont : Continuous f) (hf_bdd : ∃ M : ℝ, ∀ x, |f x| ≤ M) :
-- The PDE on (0, ∞) × ℝ.
(∀ t : ℝ, 0 < t → ∀ x : ℝ, ∃ ux : ℝ → ℝ, ∃ uxx : ℝ,
(∀ y : ℝ, HasDerivAt (fun z => heatSolution f t z) (ux y) y) ∧
HasDerivAt ux uxx x ∧
HasDerivAt (fun s => heatSolution f s x) uxx t) ∧
-- Initial condition recovered as a one-sided limit at t = 0.
(∀ x : ℝ,
Filter.Tendsto (fun t : ℝ => heatSolution f t x)
(nhdsWithin (0 : ℝ) (Set.Ioi 0)) (nhds (f x))) := f:ℝ → ℝhf_cont:Continuous fhf_bdd:∃ M, ∀ (x : ℝ), |f x| ≤ M⊢ (∀ (t : ℝ),
0 < t →
∀ (x : ℝ),
∃ ux uxx,
(∀ (y : ℝ), HasDerivAt (fun z => heatSolution f t z) (ux y) y) ∧
HasDerivAt ux uxx x ∧ HasDerivAt (fun s => heatSolution f s x) uxx t) ∧
∀ (x : ℝ), Filter.Tendsto (fun t => heatSolution f t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (f x))
All goals completed! 🐙
Minkowski-Caratheodory theorem
mem_convexHull_finset_extremePoints_of_mem_compact_convex
#196
Verso theorem preview
theorem declaration uses `sorry`mem_convexHull_finset_extremePoints_of_mem_compact_convex {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
{s : Set E} {x : E}
(hscomp : IsCompact s)
(hsconv : Convex ℝ s)
(hx : x ∈ s) :
∃ t : Finset E,
(↑t : Set E) ⊆ s.extremePoints ℝ ∧
t.card ≤ Module.finrank ℝ E + 1 ∧
x ∈ convexHull ℝ (↑t : Set E) := E:Type u_1inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:FiniteDimensional ℝ Es:Set Ex:Ehscomp:IsCompact shsconv:Convex ℝ shx:x ∈ s⊢ ∃ t, ↑t ⊆ extremePoints ℝ s ∧ t.card ≤ Module.finrank ℝ E + 1 ∧ x ∈ (convexHull ℝ) ↑t
All goals completed! 🐙
Oppenheim's inequality for Hadamard products
oppenheim_inequality
#197
Verso theorem preview
theorem declaration uses `sorry`oppenheim_inequality {n : Type*} [Fintype n] [DecidableEq n]
{A B : Matrix n n ℝ} (hA : A.PosSemidef) (hB : B.PosSemidef) :
A.det * ∏ i, B i i ≤ (A ⊙ B).det := n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝB:Matrix n n ℝhA:A.PosSemidefhB:B.PosSemidef⊢ A.det * ∏ i, B i i ≤ (A ⊙ B).det
All goals completed! 🐙
Character values of finite groups lie in cyclotomic fields
brauer_character_in_cyclotomic
#198
Verso theorem preview
theorem declaration uses `sorry`brauer_character_in_cyclotomic (G : Type) [Group G] [Fintype G] :
∃ φ : CyclotomicField (Monoid.exponent G) ℚ →+* ℂ,
∀ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V) (_ : FiniteDimensional ℂ V)
(ρ : Representation ℂ G V) (g : G),
LinearMap.trace ℂ V (ρ g) ∈ φ.range := G:Typeinst✝¹:Group Ginst✝:Fintype G⊢ ∃ φ,
∀ (V : Type) (x : AddCommGroup V) (x_1 : Module ℂ V),
FiniteDimensional ℂ V → ∀ (ρ : Representation ℂ G V) (g : G), (LinearMap.trace ℂ V) (ρ g) ∈ φ.range
All goals completed! 🐙
pi_1 of the circle is Z
pi1_circle_mulEquiv_int
#199
Verso theorem preview
theorem declaration uses `sorry`pi1_circle_mulEquiv_int :
Nonempty (HomotopyGroup.Pi 1 Circle (1 : Circle) ≃* Multiplicative ℤ) := ⊢ Nonempty (HomotopyGroup.Pi 1 Circle 1 ≃* Multiplicative ℤ)
All goals completed! 🐙
Dirichlet eigenvalues of -y'' = lambda y on [0,pi] are n^2
dirichlet_eigenvalues_eq_nat_sq
#200
Verso theorem preview
theorem declaration uses `sorry`dirichlet_eigenvalues_eq_nat_sq (lam : ℝ) :
(∃ (y : ℝ → ℝ) (J : Set ℝ),
IsOpen J ∧ Set.Icc (0 : ℝ) Real.pi ⊆ J ∧
(∀ x ∈ J, HasDerivAt y (deriv y x) x) ∧
(∀ x ∈ J, HasDerivAt (deriv y) (-(lam * y x)) x) ∧
y 0 = 0 ∧ y Real.pi = 0 ∧
∃ x ∈ Set.Ioo (0 : ℝ) Real.pi, y x ≠ 0) ↔
∃ n : ℕ, 0 < n ∧ lam = (n : ℝ) ^ 2 := lam:ℝ⊢ (∃ y J,
IsOpen J ∧
Set.Icc 0 π ⊆ J ∧
(∀ x ∈ J, HasDerivAt y (deriv y x) x) ∧
(∀ x ∈ J, HasDerivAt (deriv y) (-(lam * y x)) x) ∧ y 0 = 0 ∧ y π = 0 ∧ ∃ x ∈ Set.Ioo 0 π, y x ≠ 0) ↔
∃ n, 0 < n ∧ lam = ↑n ^ 2
All goals completed! 🐙
Entrywise exponential of a PSD matrix is PSD
posSemidef_map_exp
#201
Verso theorem preview
theorem declaration uses `sorry`posSemidef_map_exp {n : Type*} [Fintype n] [DecidableEq n]
{A : Matrix n n ℝ} (hA : A.PosSemidef) :
(A.map Real.exp).PosSemidef := n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝhA:A.PosSemidef⊢ (A.map Real.exp).PosSemidef
All goals completed! 🐙
Sturm separation theorem
sturm_separation
#202
Verso theorem preview
theorem declaration uses `sorry`sturm_separation (p q y₁ y₂ : ℝ → ℝ) (a b : ℝ) (hab : a < b)
(J : Set ℝ) (hJ_open : IsOpen J) (hJ_conn : IsPreconnected J)
(hJ_sub : Set.Icc a b ⊆ J)
(hp : ContinuousOn p J) (hq : ContinuousOn q J)
(hy₁ : ∀ x ∈ J, HasDerivAt y₁ (deriv y₁ x) x)
(hy₁' : ∀ x ∈ J, HasDerivAt (deriv y₁) (-(p x * deriv y₁ x + q x * y₁ x)) x)
(hy₂ : ∀ x ∈ J, HasDerivAt y₂ (deriv y₂ x) x)
(hy₂' : ∀ x ∈ J, HasDerivAt (deriv y₂) (-(p x * deriv y₂ x + q x * y₂ x)) x)
(hW : ∃ x₀ ∈ J, y₁ x₀ * deriv y₂ x₀ - y₂ x₀ * deriv y₁ x₀ ≠ 0)
(hza : y₁ a = 0) (hzb : y₁ b = 0)
(hne : ∀ x ∈ Set.Ioo a b, y₁ x ≠ 0) :
∃! c, c ∈ Set.Ioo a b ∧ y₂ c = 0 := p:ℝ → ℝq:ℝ → ℝy₁:ℝ → ℝy₂:ℝ → ℝa:ℝb:ℝhab:a < bJ:Set ℝhJ_open:IsOpen JhJ_conn:IsPreconnected JhJ_sub:Set.Icc a b ⊆ Jhp:ContinuousOn p Jhq:ContinuousOn q Jhy₁:∀ x ∈ J, HasDerivAt y₁ (deriv y₁ x) xhy₁':∀ x ∈ J, HasDerivAt (deriv y₁) (-(p x * deriv y₁ x + q x * y₁ x)) xhy₂:∀ x ∈ J, HasDerivAt y₂ (deriv y₂ x) xhy₂':∀ x ∈ J, HasDerivAt (deriv y₂) (-(p x * deriv y₂ x + q x * y₂ x)) xhW:∃ x₀ ∈ J, y₁ x₀ * deriv y₂ x₀ - y₂ x₀ * deriv y₁ x₀ ≠ 0hza:y₁ a = 0hzb:y₁ b = 0hne:∀ x ∈ Set.Ioo a b, y₁ x ≠ 0⊢ ∃! c, c ∈ Set.Ioo a b ∧ y₂ c = 0
All goals completed! 🐙
Polynomial decay rate of y' = -y^3
cubic_decay_asymptotic
#203
Verso theorem preview
theorem declaration uses `sorry`cubic_decay_asymptotic (y : ℝ → ℝ) (hy_diff : ∀ t : ℝ, 0 < t → HasDerivAt y (-(y t) ^ 3) t)
(hy_cont : ContinuousWithinAt y (Set.Ici 0) 0)
(hy0 : y 0 = 1) :
Tendsto (fun t : ℝ => y t * Real.sqrt t) atTop (𝓝 (1 / Real.sqrt 2)) := y:ℝ → ℝhy_diff:∀ (t : ℝ), 0 < t → HasDerivAt y (-y t ^ 3) thy_cont:ContinuousWithinAt y (Set.Ici 0) 0hy0:y 0 = 1⊢ Tendsto (fun t => y t * √t) atTop (𝓝 (1 / √2))
All goals completed! 🐙
Comparison principle for the Dirichlet BVP
bvp_comparison
#204
Verso theorem preview
theorem declaration uses `sorry`bvp_comparison (J : Set ℝ) (hJ_open : IsOpen J) (hJ_sub : Set.Icc (0 : ℝ) 1 ⊆ J)
(u v : ℝ → ℝ)
(hu : ∀ x ∈ J, HasDerivAt u (deriv u x) x)
(hu' : ∀ x ∈ J, HasDerivAt (deriv u) (deriv (deriv u) x) x)
(hv : ∀ x ∈ J, HasDerivAt v (deriv v x) x)
(hv' : ∀ x ∈ J, HasDerivAt (deriv v) (deriv (deriv v) x) x)
(hineq : ∀ x ∈ Set.Ioo (0 : ℝ) 1, -deriv (deriv u) x ≤ -deriv (deriv v) x)
(hu0 : u 0 ≤ v 0) (hu1 : u 1 ≤ v 1) :
∀ x ∈ Set.Icc (0 : ℝ) 1, u x ≤ v x := J:Set ℝhJ_open:IsOpen JhJ_sub:Set.Icc 0 1 ⊆ Ju:ℝ → ℝv:ℝ → ℝhu:∀ x ∈ J, HasDerivAt u (deriv u x) xhu':∀ x ∈ J, HasDerivAt (deriv u) (deriv (deriv u) x) xhv:∀ x ∈ J, HasDerivAt v (deriv v x) xhv':∀ x ∈ J, HasDerivAt (deriv v) (deriv (deriv v) x) xhineq:∀ x ∈ Set.Ioo 0 1, -deriv (deriv u) x ≤ -deriv (deriv v) xhu0:u 0 ≤ v 0hu1:u 1 ≤ v 1⊢ ∀ x ∈ Set.Icc 0 1, u x ≤ v x
All goals completed! 🐙
Cayley graph connected iff generators generate the group
mulCayley_connected_iff_closure_eq_top
#205
Verso theorem preview
theorem declaration uses `sorry`mulCayley_connected_iff_closure_eq_top {G : Type*} [Group G]
(S : Set G) :
(SimpleGraph.mulCayley S).Connected ↔ Subgroup.closure S = ⊤ := G:Type u_1inst✝:Group GS:Set G⊢ (SimpleGraph.mulCayley S).Connected ↔ Subgroup.closure S = ⊤
All goals completed! 🐙
Finite Ramsey theorem for graphs
finite_graph_ramsey_theorem
#206
Verso theorem preview
theorem declaration uses `sorry`finite_graph_ramsey_theorem :
∀ r s : ℕ, 2 ≤ r → 2 ≤ s → ∃ n : ℕ, ∀ G : SimpleGraph (Fin n), ¬ G.CliqueFree r ∨ ¬ Gᶜ.CliqueFree s := ⊢ ∀ (r s : ℕ), 2 ≤ r → 2 ≤ s → ∃ n, ∀ (G : SimpleGraph (Fin n)), ¬G.CliqueFree r ∨ ¬Gᶜ.CliqueFree s
All goals completed! 🐙
Catalan generating function via compositional inversion
substInv_X_sub_X_sq_eq_catalan
#207
Verso theorem preview
theorem declaration uses `sorry`substInv_X_sub_X_sq_eq_catalan (n : ℕ) :
haveI : Invertible (coeff 1 ((X : ℚ⟦X⟧) - X ^ 2)) := n:ℕ⊢ Invertible ((coeff 1) (X - X ^ 2))
n:ℕ⊢ Invertible 1; All goals completed! 🐙
coeff (n + 1) (substInv ((X : ℚ⟦X⟧) - X ^ 2)) =
(Nat.choose (2 * n) n : ℚ) / (↑n + 1) := n:ℕ⊢ (coeff (n + 1)) (X - X ^ 2).substInv = ↑((2 * n).choose n) / (↑n + 1)
All goals completed! 🐙Submission history
First submissionAug 29, 2026
Last submissionAug 29, 2026
Contributors
Vilin97207