From 3483fe2f2af19b546e3741fada7aa5d896fc5dcf Mon Sep 17 00:00:00 2001 From: leanprover-community-bot Date: Thu, 17 Oct 2024 04:08:27 +0000 Subject: [PATCH] deploy site from 0c22759bee7fa13a1084f00c519ae69d82c93384 --- 100.html | 182 ++++++++++---------- mathlib-overview.html | 4 +- mathlib_stats.html | 4 +- meet.html | 390 +++++++++++++++++++++--------------------- 4 files changed, 290 insertions(+), 290 deletions(-) diff --git a/100.html b/100.html index e6d6792ae..c799708d9 100644 --- a/100.html +++ b/100.html @@ -62,7 +62,7 @@
1. The Irrationality of the Square Root
theorem irrational_sqrt_two :
Irrational √2
-

docs, source

+

docs, source

@@ -77,7 +77,7 @@
2. Fundamental Theorem of Algebra (hf : 0 < f.degree) :
∃ (z : ℂ), f.IsRoot z
-

docs, source

+

docs, source

@@ -88,7 +88,7 @@
3. The Denumerability of the Rational N
instance Rat.instDenumerable :
Denumerable ℚ
-

docs, source

+

docs, source

@@ -117,7 +117,7 @@
4. Pythagorean Theorem (p3 : P) :
dist p1 p3 * dist p1 p3 = dist p1 p2 * dist p1 p2 + dist p3 p2 * dist p3 p2 ↔ EuclideanGeometry.angle p1 p2 p3 = Real.pi / 2
-

docs, source

+

docs, source

@@ -149,7 +149,7 @@
7. Law of Quadratic Reciprocity (hpq : p ≠ q) :
legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
-

docs, source

+

docs, source

theorem jacobiSym.quadratic_reciprocity @@ -161,7 +161,7 @@
7. Law of Quadratic Reciprocity (hb : Odd b) :
jacobiSym (↑a) b = (-1) ^ (a / 2 * (b / 2)) * jacobiSym (↑b) a
-

docs, source

+

docs, source

@@ -174,7 +174,7 @@
9. The Area of a Circle Theorems100.area_disc (r : NNReal) :
MeasureTheory.volume (Theorems100.disc ↑r) = ↑NNReal.pi * ↑r ^ 2
-

docs, source

+

docs, source

@@ -191,7 +191,7 @@
10. Euler’s Generalization of Fermat (h : x.Coprime n) :
x ^ n.totient ≡ 1 [MOD n]
-

docs, source

+

docs, source

@@ -204,7 +204,7 @@
11. The Infinitude of Primes Nat.exists_infinite_primes (n : ℕ) :
∃ (p : ℕ), n ≤ p ∧ Nat.Prime p
-

docs, source

+

docs, source

@@ -215,7 +215,7 @@
14. Euler’s Summation of 1 + (1/2)^2
theorem hasSum_zeta_two :
HasSum (fun (n : ℕ) => 1 / ↑n ^ 2) (Real.pi ^ 2 / 6)
-

docs, source

+

docs, source

@@ -248,7 +248,7 @@
15. Fundamental Theorem of Integral Ca (hb : Filter.Tendsto f (nhds b ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c)) :
HasStrictDerivAt (fun (u : ℝ) => ∫ (x : ℝ) in a..u, f x) c b
-

docs, source

+

docs, source

theorem intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le @@ -276,7 +276,7 @@
15. Fundamental Theorem of Integral Ca (f'int : IntervalIntegrable f' MeasureTheory.volume a b) :
∫ (y : ℝ) in a..b, f' y = f b - f a
-

docs, source

+

docs, source

@@ -287,7 +287,7 @@
16. Insolvability of General Higher De
theorem AbelRuffini.exists_not_solvable_by_rad :
∃ (x : ℂ), IsAlgebraic ℚ x ∧ ¬IsSolvableByRad ℚ x
-

docs, source

+

docs, source

@@ -302,7 +302,7 @@
17. De Moivre’s Formula (z : ℂ) :
(Complex.cos z + Complex.sin z * Complex.I) ^ n = Complex.cos (↑n * z) + Complex.sin (↑n * z) * Complex.I
-

docs, source

+

docs, source

@@ -317,7 +317,7 @@
18. Liouville’s Theorem and the Cons (lx : Liouville x) :
Transcendental ℤ x
-

docs, source

+

docs, source

@@ -330,7 +330,7 @@
19. Four Squares Theorem Nat.sum_four_squares (n : ℕ) :
∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ), a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n
-

docs, source

+

docs, source

@@ -347,7 +347,7 @@
20. All Primes (1 mod 4) Equal the Sum (hp : p % 4 ≠ 3) :
∃ (a : ℕ) (b : ℕ), a ^ 2 + b ^ 2 = p
-

docs, source

+

docs, source

@@ -358,7 +358,7 @@
22. The Non-Denumerability of the Cont
theorem Cardinal.not_countable_real :
¬Set.univ.Countable
-

docs, source

+

docs, source

@@ -376,7 +376,7 @@
23. Formula for Pythagorean Triples {z : ℤ} :
PythagoreanTriple x y z ↔ ∃ (k : ℤ) (m : ℤ) (n : ℤ), (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧ (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))
-

docs, source

+

docs, source

@@ -406,7 +406,7 @@
25. Schroeder-Bernstein Theorem (hg : Function.Injective g) :
∃ (h : α → β), Function.Bijective h
-

docs, source

+

docs, source

@@ -417,7 +417,7 @@
26. Leibniz’s Series for Pi
theorem Real.tendsto_sum_pi_div_four :
Filter.Tendsto (fun (k : ℕ) => ∑ i ∈ Finset.range k, (-1) ^ i / (2 * ↑i + 1)) Filter.atTop (nhds (Real.pi / 4))
-

docs, source

+

docs, source

@@ -450,7 +450,7 @@
27. Sum of the Angles of a Triangle (h3 : p3 ≠ p1) :
EuclideanGeometry.angle p1 p2 p3 + EuclideanGeometry.angle p2 p3 p1 + EuclideanGeometry.angle p3 p1 p2 = Real.pi
-

docs, source

+

docs, source

@@ -465,7 +465,7 @@
30. The Ballot Problem (p : ℕ) :
q < p → (ProbabilityTheory.uniformOn (Ballot.countedSequence p q)) Ballot.staysPositive = (↑p - ↑q) / (↑p + ↑q)
-

docs, source

+

docs, source

@@ -483,7 +483,7 @@
34. Divergence of the Harmonic Series
theorem Real.tendsto_sum_range_one_div_nat_succ_atTop :
Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, 1 / (↑i + 1)) Filter.atTop Filter.atTop
-

docs, source

+

docs, source

@@ -509,7 +509,7 @@
35. Taylor’s Theorem (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)) :
∃ x' ∈ Set.Ioo x₀ x, f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Set.Icc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1).factorial
-

docs, source

+

docs, source

theorem taylor_mean_remainder_cauchy @@ -528,7 +528,7 @@
35. Taylor’s Theorem (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)) :
∃ x' ∈ Set.Ioo x₀ x, f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Set.Icc x₀ x) x' * (x - x') ^ n / ↑n.factorial * (x - x₀)
-

docs, source

+

docs, source

@@ -592,7 +592,7 @@
37. The Solution of a Cubic (x : K) :
a * x ^ 3 + b * x ^ 2 + c * x + d = 0 ↔ x = s - t - b / (3 * a) ∨ x = s * ω - t * ω ^ 2 - b / (3 * a) ∨ x = s * ω ^ 2 - t * ω - b / (3 * a)
-

docs, source

+

docs, source

@@ -617,7 +617,7 @@
38. Arithmetic Mean/Geometric Mean (hz : ∀ i ∈ s, 0 ≤ z i) :
∏ i ∈ s, z i ^ w i ≤ ∑ i ∈ s, w i * z i
-

docs, source

+

docs, source

@@ -638,7 +638,7 @@
39. Solutions to Pell’s Equation (hp : x * x - Pell.d a1 * y * y = 1) :
∃ (n : ℕ), x = Pell.xn a1 n ∧ y = Pell.yn a1 n
-

docs, source

+

docs, source

theorem Pell.exists_of_not_isSquare @@ -648,7 +648,7 @@
39. Solutions to Pell’s Equation (hd : ¬IsSquare d) :
∃ (x : ℤ) (y : ℤ), x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
-

docs, source

+

docs, source

In pell.eq_pell, d is defined to be a*a - 1 for an arbitrary a > 1.

@@ -691,7 +691,7 @@
40. Minkowski’s Fundamental Theorem (h : μ F * 2 ^ Module.finrank ℝ E < μ s) :
∃ (x : ↥L), x ≠ 0 ∧ ↑x ∈ s
-

docs, source

+

docs, source

@@ -704,7 +704,7 @@
42. Sum of the Reciprocals of the Tria Theorems100.inverse_triangle_sum (n : ℕ) :
∑ k ∈ Finset.range n, 2 / (↑k * (↑k + 1)) = if n = 0 then 0 else 2 - 2 / ↑n
-

docs, source

+

docs, source

@@ -725,7 +725,7 @@
44. The Binomial Theorem (n : ℕ) :
(x + y) ^ n = ∑ m ∈ Finset.range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)
-

docs, source

+

docs, source

@@ -738,7 +738,7 @@
45. The Partition Theorem Theorems100.partition_theorem (n : ℕ) :
(Nat.Partition.odds n).card = (Nat.Partition.distincts n).card
-

docs, source

+

docs, source

@@ -761,7 +761,7 @@
49. The Cayley-Hamilton Theorem (M : Matrix n n R) :
(Polynomial.aeval M) M.charpoly = 0
-

docs, source

+

docs, source

@@ -776,7 +776,7 @@
51. Wilson’s Lemma [Fact (Nat.Prime p)] :
↑(p - 1).factorial = -1
-

docs, source

+

docs, source

@@ -791,7 +791,7 @@
52. The Number of Subsets of a Set (s : Finset α) :
s.powerset.card = 2 ^ s.card
-

docs, source

+

docs, source

@@ -810,7 +810,7 @@
54. Königsberg Bridges Problem (h : p.IsEulerian) :
False
-

docs, source

+

docs, source

@@ -849,7 +849,7 @@
55. Product of Segments of Chords (hcpd : EuclideanGeometry.angle c p d = Real.pi) :
dist a p * dist b p = dist c p * dist d p
-

docs, source

+

docs, source

@@ -886,7 +886,7 @@
57. Heron’s Formula let c := dist p1 p3; let s := (a + b + c) / 2; 1 / 2 * a * b * Real.sin (EuclideanGeometry.angle p1 p2 p3) = √(s * (s - a) * (s - b) * (s - c)) -

docs, source

+

docs, source

@@ -903,7 +903,7 @@
58. Formula for the Number of Combinat (s : Finset α) :
(Finset.powersetCard n s).card = s.card.choose n
-

docs, source

+

docs, source

theorem Finset.mem_powersetCard @@ -915,7 +915,7 @@
58. Formula for the Number of Combinat {t : Finset α} :
s ∈ Finset.powersetCard n t ↔ s ⊆ t ∧ s.card = n
-

docs, source

+

docs, source

@@ -953,7 +953,7 @@
59. The Laws of Large Numbers (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) :
∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) Filter.atTop (nhds (∫ (x : Ω), X 0 x ∂μ))
-

docs, source

+

docs, source

@@ -968,7 +968,7 @@
60. Bezout’s Theorem (y : ℕ) :
↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y
-

docs, source

+

docs, source

@@ -1000,7 +1000,7 @@
62. Fair Games Theorem τ ≤ π → (∃ (N : ℕ), ∀ (x : Ω), π x ≤ N) → ∫ (x : Ω), MeasureTheory.stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), MeasureTheory.stoppedValue f π x ∂μ -

docs, source

+

docs, source

@@ -1013,7 +1013,7 @@
63. Cantor’s Theorem Cardinal.cantor (a : Cardinal.{u}) :
a < 2 ^ a
-

docs, source

+

docs, source

@@ -1042,7 +1042,7 @@
64. L’Hopital’s Rule (hdiv : Filter.Tendsto (fun (x : ℝ) => deriv f x / deriv g x) (nhds a) l) :
Filter.Tendsto (fun (x : ℝ) => f x / g x) (nhdsWithin a {a}ᶜ) l
-

docs, source

+

docs, source

@@ -1073,7 +1073,7 @@
65. Isosceles Triangle Theorem (h : dist p1 p2 = dist p1 p3) :
EuclideanGeometry.angle p1 p2 p3 = EuclideanGeometry.angle p1 p3 p2
-

docs, source

+

docs, source

@@ -1098,7 +1098,7 @@
66. Sum of a Geometric Series (hmn : m ≤ n) :
∑ i ∈ Finset.Ico m n, x ^ i = (x ^ n - x ^ m) / (x - 1)
-

docs, source

+

docs, source

theorem NNReal.hasSum_geometric @@ -1106,7 +1106,7 @@
66. Sum of a Geometric Series (hr : r < 1) :
HasSum (fun (n : ℕ) => r ^ n) (1 - r)⁻¹
-

docs, source

+

docs, source

@@ -1126,7 +1126,7 @@
68. Sum of an arithmetic series Finset.sum_range_id (n : ℕ) :
∑ i ∈ Finset.range n, i = n * (n - 1) / 2
-

docs, source

+

docs, source

@@ -1147,7 +1147,7 @@
69. Greatest Common Divisor Algorithm (b : R) :
R
-

docs, source

+

docs, source

theorem EuclideanDomain.gcd_dvd @@ -1161,7 +1161,7 @@
69. Greatest Common Divisor Algorithm (b : R) :
EuclideanDomain.gcd a b ∣ a ∧ EuclideanDomain.gcd a b ∣ b
-

docs, source

+

docs, source

theorem EuclideanDomain.dvd_gcd @@ -1177,7 +1177,7 @@
69. Greatest Common Divisor Algorithm {c : R} :
c ∣ a → c ∣ b → c ∣ EuclideanDomain.gcd a b
-

docs, source

+

docs, source

@@ -1194,7 +1194,7 @@
70. The Perfect Number Theorem (perf : n.Perfect) :
∃ (k : ℕ), Nat.Prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1)
-

docs, source

+

docs, source

@@ -1211,7 +1211,7 @@
71. Order of a Subgroup (s : Subgroup α) :
Nat.card ↥s ∣ Nat.card α
-

docs, source

+

docs, source

@@ -1236,7 +1236,7 @@
72. Sylow’s Theorem (hdvd : p ^ n ∣ Nat.card G) :
∃ (K : Subgroup G), Nat.card ↥K = p ^ n
-

docs, source

+

docs, source

sylow_conjugate

card_sylow_dvd

card_sylow_modeq_one

@@ -1263,7 +1263,7 @@
73. Ascending or Descending Sequences (hf : Function.Injective f) :
(∃ (t : Finset (Fin n)), r < t.card ∧ StrictMonoOn f ↑t) ∨ ∃ (t : Finset (Fin n)), s < t.card ∧ StrictAntiOn f ↑t
-

docs, source

+

docs, source

@@ -1297,7 +1297,7 @@
75. The Mean Value Theorem (hfd : DifferentiableOn ℝ f (Set.Ioo a b)) :
∃ c ∈ Set.Ioo a b, deriv f c = (f b - f a) / (b - a)
-

docs, source

+

docs, source

@@ -1322,7 +1322,7 @@
76. Fourier Series (n : ℤ) :
E
-

docs, source

+

docs, source

theorem hasSum_fourier_series_L2 @@ -1332,7 +1332,7 @@
76. Fourier Series (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) :
HasSum (fun (i : ℤ) => fourierCoeff (↑↑f) i • fourierLp 2 i) f
-

docs, source

+

docs, source

@@ -1347,7 +1347,7 @@
77. Sum of kth powers (p : ℕ) :
∑ k ∈ Finset.range n, ↑k ^ p = ∑ i ∈ Finset.range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)
-

docs, source

+

docs, source

theorem sum_Ico_pow @@ -1355,7 +1355,7 @@
77. Sum of kth powers (p : ℕ) :
∑ k ∈ Finset.Ico 1 (n + 1), ↑k ^ p = ∑ i ∈ Finset.range (p + 1), bernoulli' i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)
-

docs, source

+

docs, source

@@ -1380,7 +1380,7 @@
78. The Cauchy-Schwarz Inequality (y : E) :
‖inner x y‖ * ‖inner y x‖ ≤ RCLike.re (inner x x) * RCLike.re (inner y y)
-

docs, source

+

docs, source

theorem norm_inner_le_norm @@ -1398,7 +1398,7 @@
78. The Cauchy-Schwarz Inequality (y : E) :
‖inner x y‖ ≤ ‖x‖ * ‖y‖
-

docs, source

+

docs, source

@@ -1437,7 +1437,7 @@
79. The Intermediate Value Theorem (hf : ContinuousOn f (Set.Icc a b)) :
Set.Icc (f a) (f b) ⊆ f '' Set.Icc a b
-

docs, source

+

docs, source

@@ -1456,11 +1456,11 @@
80. The Fundamental Theorem of Arithme (h₂ : ∀ p ∈ l, Nat.Prime p) :
l.Perm n.primeFactorsList
-

docs, source

+

docs, source

instance Int.euclideanDomain :
EuclideanDomain ℤ
-

docs, source

+

docs, source

instance EuclideanDomain.to_principal_ideal_domain @@ -1468,7 +1468,7 @@
80. The Fundamental Theorem of Arithme [EuclideanDomain R] :
IsPrincipalIdealRing R
-

docs, source

+

docs, source

class UniqueFactorizationMonoid @@ -1478,7 +1478,7 @@
80. The Fundamental Theorem of Arithme extends IsWellFounded :
Prop
-

docs, source

+

docs, source

theorem UniqueFactorizationMonoid.factors_unique @@ -1498,7 +1498,7 @@
80. The Fundamental Theorem of Arithme (h : Associated f.prod g.prod) :
Multiset.Rel Associated f g
-

docs, source

+

docs, source

it also has a generalized version, by showing that every Euclidean domain is a unique factorization domain, and showing that the integers form a Euclidean domain.

@@ -1510,11 +1510,11 @@
81. Divergence of the Prime Reciprocal
theorem Theorems100.Real.tendsto_sum_one_div_prime_atTop :
Filter.Tendsto (fun (n : ℕ) => ∑ p ∈ Finset.filter (fun (p : ℕ) => Nat.Prime p) (Finset.range n), 1 / ↑p) Filter.atTop Filter.atTop
-

docs, source

+

docs, source

theorem not_summable_one_div_on_primes :
¬Summable ({p : ℕ | Nat.Prime p}.indicator fun (n : ℕ) => 1 / ↑n)
-

docs, source

+

docs, source

@@ -1532,7 +1532,7 @@
82. Dissection of Cubes (J.E. Littlewo s.Nontrivial → s.PairwiseDisjoint Theorems100.«82».Cube.toSet → ⋃ c ∈ s, c.toSet = Theorems100.«82».Cube.unitCube.toSet → Set.InjOn Theorems100.«82».Cube.w s → False -

docs, source

+

docs, source

@@ -1553,7 +1553,7 @@
83. The Friendship Theorem [Nonempty V] :
Theorems100.ExistsPolitician G
-

docs, source

+

docs, source

@@ -1566,7 +1566,7 @@
85. Divisibility by 3 Rule Nat.three_dvd_iff (n : ℕ) :
3 ∣ n ↔ 3 ∣ (Nat.digits 10 n).sum
-

docs, source

+

docs, source

@@ -1579,7 +1579,7 @@
86. Lebesgue Measure and Integration < MeasureTheory.lintegral {α : Type u_5} :
{x : MeasurableSpace α} → MeasureTheory.Measure α → (α → ENNReal) → ENNReal
-

docs, source

+

docs, source

@@ -1596,13 +1596,13 @@
88. Derangements Formula [DecidableEq α] :
Fintype.card ↑(derangements α) = numDerangements (Fintype.card α)
-

docs, source

+

docs, source

theorem numDerangements_sum (n : ℕ) :
↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
-

docs, source

+

docs, source

@@ -1621,7 +1621,7 @@
89. The Factor and Remainder Theorems {p : Polynomial R} :
Polynomial.X - Polynomial.C a ∣ p ↔ p.IsRoot a
-

docs, source

+

docs, source

theorem Polynomial.mod_X_sub_C_eq_C_eval @@ -1633,7 +1633,7 @@
89. The Factor and Remainder Theorems (a : R) :
p % (Polynomial.X - Polynomial.C a) = Polynomial.C (Polynomial.eval a p)
-

docs, source

+

docs, source

@@ -1644,7 +1644,7 @@
90. Stirling’s Formula
theorem Stirling.tendsto_stirlingSeq_sqrt_pi :
Filter.Tendsto Stirling.stirlingSeq Filter.atTop (nhds √Real.pi)
-

docs, source

+

docs, source

@@ -1663,7 +1663,7 @@
91. The Triangle Inequality (b : E) :
‖a + b‖ ≤ ‖a‖ + ‖b‖
-

docs, source

+

docs, source

@@ -1674,11 +1674,11 @@
93. The Birthday Problem
theorem Theorems100.birthday :
2 * Fintype.card (Fin 23 ↪ Fin 365) < Fintype.card (Fin 23 → Fin 365) ∧ 2 * Fintype.card (Fin 22 ↪ Fin 365) > Fintype.card (Fin 22 → Fin 365)
-

docs, source

+

docs, source

theorem Theorems100.birthday_measure :
MeasureTheory.volume {f : Fin 23 → Fin 365 | Function.Injective f} < 1 / 2
-

docs, source

+

docs, source

@@ -1707,7 +1707,7 @@
94. The Law of Cosines (p3 : P) :
dist p1 p3 * dist p1 p3 = dist p1 p2 * dist p1 p2 + dist p3 p2 * dist p3 p2 - 2 * dist p1 p2 * dist p3 p2 * Real.cos (EuclideanGeometry.angle p1 p2 p3)
-

docs, source

+

docs, source

@@ -1746,7 +1746,7 @@
95. Ptolemy’s Theorem (hbpd : EuclideanGeometry.angle b p d = Real.pi) :
dist a b * dist c d + dist b c * dist d a = dist a c * dist b d
-

docs, source

+

docs, source

@@ -1778,7 +1778,7 @@
97. Cramer’s Rule (b : n → α) :
A.mulVec (A.cramer b) = A.det • b
-

docs, source

+

docs, source

@@ -1793,7 +1793,7 @@
98. Bertrand’s Postulate (hn0 : n ≠ 0) :
∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
-

docs, source

+

docs, source

@@ -1824,7 +1824,7 @@
99. Buffon Needle Problem (h : l ≤ d) :
∫ (x : Ω), BuffonsNeedle.N l B x = 2 * l * (d * Real.pi)⁻¹
-

docs, source

+

docs, source

theorem BuffonsNeedle.buffon_long @@ -1848,7 +1848,7 @@
99. Buffon Needle Problem (h : d ≤ l) :
∫ (x : Ω), BuffonsNeedle.N l B x = 2 * l / (d * Real.pi) - 2 / (d * Real.pi) * (√(l ^ 2 - d ^ 2) + d * Real.arcsin (d / l)) + 1
-

docs, source

+

docs, source

diff --git a/mathlib-overview.html b/mathlib-overview.html index a209c3129..9d34cac9e 100644 --- a/mathlib-overview.html +++ b/mathlib-overview.html @@ -1158,7 +1158,7 @@

Data structuresarray, - difference list, + difference list, lazy list, @@ -1192,7 +1192,7 @@

Data structuresred-black map, - hash map, + hash map, finitely supported function, diff --git a/mathlib_stats.html b/mathlib_stats.html index 491ac7d9d..c737defd2 100644 --- a/mathlib_stats.html +++ b/mathlib_stats.html @@ -60,8 +60,8 @@

Counts

Contributors - 86487 - 169373 + 86595 + 167174 341 diff --git a/meet.html b/meet.html index d0c2f7f4f..2abcc251f 100644 --- a/meet.html +++ b/meet.html @@ -296,6 +296,18 @@
Contributing
marker_right.bindPopup("Stefan Hetzl
GitHub: shetzl"); markers.addLayer(marker_right); +var marker = L.marker([46.3159, 7.9878]); +marker.bindPopup("David Loeffler"); +markers.addLayer(marker); + +var marker_left = L.marker([46.3159, -352.0122]); +marker_left.bindPopup("David Loeffler"); +markers.addLayer(marker_left); + +var marker_right = L.marker([46.3159, 367.9878]); +marker_right.bindPopup("David Loeffler"); +markers.addLayer(marker_right); + var marker = L.marker([35.713447207515834, 139.76230247682759]); marker.bindPopup("Kazuki Takashima
GitHub: kzk-program"); markers.addLayer(marker); @@ -332,18 +344,6 @@
Contributing
marker_right.bindPopup("Kyle Miller
GitHub: kmill"); markers.addLayer(marker_right); -var marker = L.marker([52.237049, 21.017532]); -marker.bindPopup("Marcin Wojnarowski
GitHub: shilangyu"); -markers.addLayer(marker); - -var marker_left = L.marker([52.237049, -338.982468]); -marker_left.bindPopup("Marcin Wojnarowski
GitHub: shilangyu"); -markers.addLayer(marker_left); - -var marker_right = L.marker([52.237049, 381.017532]); -marker_right.bindPopup("Marcin Wojnarowski
GitHub: shilangyu"); -markers.addLayer(marker_right); - var marker = L.marker([49.4172736001205, 8.67570384259312]); marker.bindPopup("Flo (Florent Schaffhauser)"); markers.addLayer(marker); @@ -380,40 +380,28 @@
Contributing
marker_right.bindPopup("Josha Dekker
GitHub: JADekker"); markers.addLayer(marker_right); -var marker = L.marker([33.99825, -81.02549]); -marker.bindPopup("Matthew Ballard
GitHub: mattrobball"); -markers.addLayer(marker); - -var marker_left = L.marker([33.99825, -441.02549]); -marker_left.bindPopup("Matthew Ballard
GitHub: mattrobball"); -markers.addLayer(marker_left); - -var marker_right = L.marker([33.99825, 278.97451]); -marker_right.bindPopup("Matthew Ballard
GitHub: mattrobball"); -markers.addLayer(marker_right); - -var marker = L.marker([47.559601, 7.588576]); -marker.bindPopup("Sarah Laplace
GitHub: sblaplace"); +var marker = L.marker([52.237049, 21.017532]); +marker.bindPopup("Marcin Wojnarowski
GitHub: shilangyu"); markers.addLayer(marker); -var marker_left = L.marker([47.559601, -352.411424]); -marker_left.bindPopup("Sarah Laplace
GitHub: sblaplace"); +var marker_left = L.marker([52.237049, -338.982468]); +marker_left.bindPopup("Marcin Wojnarowski
GitHub: shilangyu"); markers.addLayer(marker_left); -var marker_right = L.marker([47.559601, 367.588576]); -marker_right.bindPopup("Sarah Laplace
GitHub: sblaplace"); +var marker_right = L.marker([52.237049, 381.017532]); +marker_right.bindPopup("Marcin Wojnarowski
GitHub: shilangyu"); markers.addLayer(marker_right); -var marker = L.marker([-22.932126, -43.243052]); -marker.bindPopup("Thiago Andrade
GitHub: 01tpaabr"); +var marker = L.marker([33.99825, -81.02549]); +marker.bindPopup("Matthew Ballard
GitHub: mattrobball"); markers.addLayer(marker); -var marker_left = L.marker([-22.932126, -403.243052]); -marker_left.bindPopup("Thiago Andrade
GitHub: 01tpaabr"); +var marker_left = L.marker([33.99825, -441.02549]); +marker_left.bindPopup("Matthew Ballard
GitHub: mattrobball"); markers.addLayer(marker_left); -var marker_right = L.marker([-22.932126, 316.756948]); -marker_right.bindPopup("Thiago Andrade
GitHub: 01tpaabr"); +var marker_right = L.marker([33.99825, 278.97451]); +marker_right.bindPopup("Matthew Ballard
GitHub: mattrobball"); markers.addLayer(marker_right); var marker = L.marker([49.7934, 9.9328]); @@ -464,6 +452,30 @@
Contributing
marker_right.bindPopup("Derek Rhodes
GitHub: drhodes"); markers.addLayer(marker_right); +var marker = L.marker([47.559601, 7.588576]); +marker.bindPopup("Sarah Laplace
GitHub: sblaplace"); +markers.addLayer(marker); + +var marker_left = L.marker([47.559601, -352.411424]); +marker_left.bindPopup("Sarah Laplace
GitHub: sblaplace"); +markers.addLayer(marker_left); + +var marker_right = L.marker([47.559601, 367.588576]); +marker_right.bindPopup("Sarah Laplace
GitHub: sblaplace"); +markers.addLayer(marker_right); + +var marker = L.marker([-22.932126, -43.243052]); +marker.bindPopup("Thiago Andrade
GitHub: 01tpaabr"); +markers.addLayer(marker); + +var marker_left = L.marker([-22.932126, -403.243052]); +marker_left.bindPopup("Thiago Andrade
GitHub: 01tpaabr"); +markers.addLayer(marker_left); + +var marker_right = L.marker([-22.932126, 316.756948]); +marker_right.bindPopup("Thiago Andrade
GitHub: 01tpaabr"); +markers.addLayer(marker_right); + var marker = L.marker([37.7889, 122.3982]); marker.bindPopup("Kyle Ellefsen
GitHub: kyleellefsen"); markers.addLayer(marker); @@ -500,6 +512,102 @@
Contributing
marker_right.bindPopup("Sébastien Gouëzel
GitHub: sgouezel"); markers.addLayer(marker_right); +var marker = L.marker([42.373756, -71.100806]); +marker.bindPopup("Daniel Windham
GitHub: tenedor"); +markers.addLayer(marker); + +var marker_left = L.marker([42.373756, -431.10080600000003]); +marker_left.bindPopup("Daniel Windham
GitHub: tenedor"); +markers.addLayer(marker_left); + +var marker_right = L.marker([42.373756, 288.89919399999997]); +marker_right.bindPopup("Daniel Windham
GitHub: tenedor"); +markers.addLayer(marker_right); + +var marker = L.marker([51.3397, 12.3731]); +marker.bindPopup("Abhiram M K
GitHub: abhirammk"); +markers.addLayer(marker); + +var marker_left = L.marker([51.3397, -347.6269]); +marker_left.bindPopup("Abhiram M K
GitHub: abhirammk"); +markers.addLayer(marker_left); + +var marker_right = L.marker([51.3397, 372.3731]); +marker_right.bindPopup("Abhiram M K
GitHub: abhirammk"); +markers.addLayer(marker_right); + +var marker = L.marker([53.568059, 9.974478]); +marker.bindPopup("Roman Stehling"); +markers.addLayer(marker); + +var marker_left = L.marker([53.568059, -350.025522]); +marker_left.bindPopup("Roman Stehling"); +markers.addLayer(marker_left); + +var marker_right = L.marker([53.568059, 369.974478]); +marker_right.bindPopup("Roman Stehling"); +markers.addLayer(marker_right); + +var marker = L.marker([12.9716, 77.5946]); +marker.bindPopup("Mrigank Pawagi
GitHub: mrigankpawagi"); +markers.addLayer(marker); + +var marker_left = L.marker([12.9716, -282.4054]); +marker_left.bindPopup("Mrigank Pawagi
GitHub: mrigankpawagi"); +markers.addLayer(marker_left); + +var marker_right = L.marker([12.9716, 437.5946]); +marker_right.bindPopup("Mrigank Pawagi
GitHub: mrigankpawagi"); +markers.addLayer(marker_right); + +var marker = L.marker([39.7392, -104.9903]); +marker.bindPopup("Chance Nahuway
GitHub: chancenahuway"); +markers.addLayer(marker); + +var marker_left = L.marker([39.7392, -464.9903]); +marker_left.bindPopup("Chance Nahuway
GitHub: chancenahuway"); +markers.addLayer(marker_left); + +var marker_right = L.marker([39.7392, 255.0097]); +marker_right.bindPopup("Chance Nahuway
GitHub: chancenahuway"); +markers.addLayer(marker_right); + +var marker = L.marker([47.610609, -122.182161]); +marker.bindPopup("Jair Taylor"); +markers.addLayer(marker); + +var marker_left = L.marker([47.610609, -482.182161]); +marker_left.bindPopup("Jair Taylor"); +markers.addLayer(marker_left); + +var marker_right = L.marker([47.610609, 237.817839]); +marker_right.bindPopup("Jair Taylor"); +markers.addLayer(marker_right); + +var marker = L.marker([51.05011, -114.08529]); +marker.bindPopup("Hal Heinrich
GitHub: halheinrich"); +markers.addLayer(marker); + +var marker_left = L.marker([51.05011, -474.08529]); +marker_left.bindPopup("Hal Heinrich
GitHub: halheinrich"); +markers.addLayer(marker_left); + +var marker_right = L.marker([51.05011, 245.91471]); +marker_right.bindPopup("Hal Heinrich
GitHub: halheinrich"); +markers.addLayer(marker_right); + +var marker = L.marker([41.852507, 12.603816]); +marker.bindPopup("Rafael Leon Greenblatt
GitHub: RafaelGreenblatt"); +markers.addLayer(marker); + +var marker_left = L.marker([41.852507, -347.396184]); +marker_left.bindPopup("Rafael Leon Greenblatt
GitHub: RafaelGreenblatt"); +markers.addLayer(marker_left); + +var marker_right = L.marker([41.852507, 372.603816]); +marker_right.bindPopup("Rafael Leon Greenblatt
GitHub: RafaelGreenblatt"); +markers.addLayer(marker_right); + var marker = L.marker([48.138534, 11.576959]); marker.bindPopup("Marc Huisinga
GitHub: mhuisi"); markers.addLayer(marker); @@ -512,6 +620,18 @@
Contributing
marker_right.bindPopup("Marc Huisinga
GitHub: mhuisi"); markers.addLayer(marker_right); +var marker = L.marker([43.8563, 18.4131]); +marker.bindPopup("Atif Degirmendzic"); +markers.addLayer(marker); + +var marker_left = L.marker([43.8563, -341.5869]); +marker_left.bindPopup("Atif Degirmendzic"); +markers.addLayer(marker_left); + +var marker_right = L.marker([43.8563, 378.4131]); +marker_right.bindPopup("Atif Degirmendzic"); +markers.addLayer(marker_right); + var marker = L.marker([55.944779, -3.187372]); marker.bindPopup("Ramon Fernández Mir"); markers.addLayer(marker); @@ -548,6 +668,18 @@
Contributing
marker_right.bindPopup("Daniel Carranza
GitHub: daniel-carranza"); markers.addLayer(marker_right); +var marker = L.marker([50.417524, -104.591557]); +marker.bindPopup("Joey Eremondi
GitHub: JoeyEremondi"); +markers.addLayer(marker); + +var marker_left = L.marker([50.417524, -464.59155699999997]); +marker_left.bindPopup("Joey Eremondi
GitHub: JoeyEremondi"); +markers.addLayer(marker_left); + +var marker_right = L.marker([50.417524, 255.408443]); +marker_right.bindPopup("Joey Eremondi
GitHub: JoeyEremondi"); +markers.addLayer(marker_right); + var marker = L.marker([41.715137, 44.827095]); marker.bindPopup("Evgenia Karunus
GitHub: lakesare"); markers.addLayer(marker); @@ -584,6 +716,18 @@
Contributing
marker_right.bindPopup("Henrique Coelho"); markers.addLayer(marker_right); +var marker = L.marker([48.262587, 11.667908]); +marker.bindPopup("Andreas Vollert
GitHub: hydrogenoxide"); +markers.addLayer(marker); + +var marker_left = L.marker([48.262587, -348.332092]); +marker_left.bindPopup("Andreas Vollert
GitHub: hydrogenoxide"); +markers.addLayer(marker_left); + +var marker_right = L.marker([48.262587, 371.667908]); +marker_right.bindPopup("Andreas Vollert
GitHub: hydrogenoxide"); +markers.addLayer(marker_right); + var marker = L.marker([26.3088521, 50.1428595]); marker.bindPopup("Khaled Alshehri"); markers.addLayer(marker); @@ -608,18 +752,6 @@
Contributing
marker_right.bindPopup("Dragan Okanovic
GitHub: abstractalgo"); markers.addLayer(marker_right); -var marker = L.marker([42.373756, -71.100806]); -marker.bindPopup("Daniel Windham
GitHub: tenedor"); -markers.addLayer(marker); - -var marker_left = L.marker([42.373756, -431.10080600000003]); -marker_left.bindPopup("Daniel Windham
GitHub: tenedor"); -markers.addLayer(marker_left); - -var marker_right = L.marker([42.373756, 288.89919399999997]); -marker_right.bindPopup("Daniel Windham
GitHub: tenedor"); -markers.addLayer(marker_right); - var marker = L.marker([40.015, 105.2705]); marker.bindPopup("Brian W Bush
GitHub: bwbush"); markers.addLayer(marker); @@ -632,28 +764,16 @@
Contributing
marker_right.bindPopup("Brian W Bush
GitHub: bwbush"); markers.addLayer(marker_right); -var marker = L.marker([51.3397, 12.3731]); -marker.bindPopup("Abhiram M K
GitHub: abhirammk"); -markers.addLayer(marker); - -var marker_left = L.marker([51.3397, -347.6269]); -marker_left.bindPopup("Abhiram M K
GitHub: abhirammk"); -markers.addLayer(marker_left); - -var marker_right = L.marker([51.3397, 372.3731]); -marker_right.bindPopup("Abhiram M K
GitHub: abhirammk"); -markers.addLayer(marker_right); - -var marker = L.marker([53.568059, 9.974478]); -marker.bindPopup("Roman Stehling"); +var marker = L.marker([20.173226, 85.684102]); +marker.bindPopup("Abhijit Chakraborty
GitHub: Abhijit-niser"); markers.addLayer(marker); -var marker_left = L.marker([53.568059, -350.025522]); -marker_left.bindPopup("Roman Stehling"); +var marker_left = L.marker([20.173226, -274.315898]); +marker_left.bindPopup("Abhijit Chakraborty
GitHub: Abhijit-niser"); markers.addLayer(marker_left); -var marker_right = L.marker([53.568059, 369.974478]); -marker_right.bindPopup("Roman Stehling"); +var marker_right = L.marker([20.173226, 445.684102]); +marker_right.bindPopup("Abhijit Chakraborty
GitHub: Abhijit-niser"); markers.addLayer(marker_right); var marker = L.marker([52.087216, 5.165171]); @@ -668,64 +788,16 @@
Contributing
marker_right.bindPopup("Edward van de Meent
GitHub: blizzard_inc"); markers.addLayer(marker_right); -var marker = L.marker([46.3159, 7.9878]); -marker.bindPopup("David Loeffler"); -markers.addLayer(marker); - -var marker_left = L.marker([46.3159, -352.0122]); -marker_left.bindPopup("David Loeffler"); -markers.addLayer(marker_left); - -var marker_right = L.marker([46.3159, 367.9878]); -marker_right.bindPopup("David Loeffler"); -markers.addLayer(marker_right); - -var marker = L.marker([12.9716, 77.5946]); -marker.bindPopup("Mrigank Pawagi
GitHub: mrigankpawagi"); -markers.addLayer(marker); - -var marker_left = L.marker([12.9716, -282.4054]); -marker_left.bindPopup("Mrigank Pawagi
GitHub: mrigankpawagi"); -markers.addLayer(marker_left); - -var marker_right = L.marker([12.9716, 437.5946]); -marker_right.bindPopup("Mrigank Pawagi
GitHub: mrigankpawagi"); -markers.addLayer(marker_right); - -var marker = L.marker([39.7392, -104.9903]); -marker.bindPopup("Chance Nahuway
GitHub: chancenahuway"); -markers.addLayer(marker); - -var marker_left = L.marker([39.7392, -464.9903]); -marker_left.bindPopup("Chance Nahuway
GitHub: chancenahuway"); -markers.addLayer(marker_left); - -var marker_right = L.marker([39.7392, 255.0097]); -marker_right.bindPopup("Chance Nahuway
GitHub: chancenahuway"); -markers.addLayer(marker_right); - -var marker = L.marker([47.610609, -122.182161]); -marker.bindPopup("Jair Taylor"); -markers.addLayer(marker); - -var marker_left = L.marker([47.610609, -482.182161]); -marker_left.bindPopup("Jair Taylor"); -markers.addLayer(marker_left); - -var marker_right = L.marker([47.610609, 237.817839]); -marker_right.bindPopup("Jair Taylor"); -markers.addLayer(marker_right); - -var marker = L.marker([51.05011, -114.08529]); -marker.bindPopup("Hal Heinrich
GitHub: halheinrich"); +var marker = L.marker([37.55, -121.99]); +marker.bindPopup("Anirudh Rao
GitHub: rao107"); markers.addLayer(marker); -var marker_left = L.marker([51.05011, -474.08529]); -marker_left.bindPopup("Hal Heinrich
GitHub: halheinrich"); +var marker_left = L.marker([37.55, -481.99]); +marker_left.bindPopup("Anirudh Rao
GitHub: rao107"); markers.addLayer(marker_left); -var marker_right = L.marker([51.05011, 245.91471]); -marker_right.bindPopup("Hal Heinrich
GitHub: halheinrich"); +var marker_right = L.marker([37.55, 238.01]); +marker_right.bindPopup("Anirudh Rao
GitHub: rao107"); markers.addLayer(marker_right); var marker = L.marker([37.571, 126.977]); @@ -752,18 +824,6 @@
Contributing
marker_right.bindPopup("Ashley Blacquiere
GitHub: ashandoak"); markers.addLayer(marker_right); -var marker = L.marker([41.852507, 12.603816]); -marker.bindPopup("Rafael Leon Greenblatt
GitHub: RafaelGreenblatt"); -markers.addLayer(marker); - -var marker_left = L.marker([41.852507, -347.396184]); -marker_left.bindPopup("Rafael Leon Greenblatt
GitHub: RafaelGreenblatt"); -markers.addLayer(marker_left); - -var marker_right = L.marker([41.852507, 372.603816]); -marker_right.bindPopup("Rafael Leon Greenblatt
GitHub: RafaelGreenblatt"); -markers.addLayer(marker_right); - var marker = L.marker([52.334811, 4.864481]); marker.bindPopup("Sander Dahmen"); markers.addLayer(marker); @@ -812,18 +872,6 @@
Contributing
marker_right.bindPopup("Dom Verity
GitHub: dom-verity@github.com"); markers.addLayer(marker_right); -var marker = L.marker([43.8563, 18.4131]); -marker.bindPopup("Atif Degirmendzic"); -markers.addLayer(marker); - -var marker_left = L.marker([43.8563, -341.5869]); -marker_left.bindPopup("Atif Degirmendzic"); -markers.addLayer(marker_left); - -var marker_right = L.marker([43.8563, 378.4131]); -marker_right.bindPopup("Atif Degirmendzic"); -markers.addLayer(marker_right); - var marker = L.marker([59.9405, 10.7217496]); marker.bindPopup("Torger Olson"); markers.addLayer(marker); @@ -872,18 +920,6 @@
Contributing
marker_right.bindPopup("Jireh Loreaux
GitHub: j-loreaux"); markers.addLayer(marker_right); -var marker = L.marker([50.417524, -104.591557]); -marker.bindPopup("Joey Eremondi
GitHub: JoeyEremondi"); -markers.addLayer(marker); - -var marker_left = L.marker([50.417524, -464.59155699999997]); -marker_left.bindPopup("Joey Eremondi
GitHub: JoeyEremondi"); -markers.addLayer(marker_left); - -var marker_right = L.marker([50.417524, 255.408443]); -marker_right.bindPopup("Joey Eremondi
GitHub: JoeyEremondi"); -markers.addLayer(marker_right); - var marker = L.marker([42.450528451924626, -76.48143612664352]); marker.bindPopup("Samuel Homiller
GitHub: shomiller"); markers.addLayer(marker); @@ -896,18 +932,6 @@
Contributing
marker_right.bindPopup("Samuel Homiller
GitHub: shomiller"); markers.addLayer(marker_right); -var marker = L.marker([48.262587, 11.667908]); -marker.bindPopup("Andreas Vollert
GitHub: hydrogenoxide"); -markers.addLayer(marker); - -var marker_left = L.marker([48.262587, -348.332092]); -marker_left.bindPopup("Andreas Vollert
GitHub: hydrogenoxide"); -markers.addLayer(marker_left); - -var marker_right = L.marker([48.262587, 371.667908]); -marker_right.bindPopup("Andreas Vollert
GitHub: hydrogenoxide"); -markers.addLayer(marker_right); - var marker = L.marker([52.22977, 21.01178]); marker.bindPopup("Wojciech Nawrocki"); markers.addLayer(marker); @@ -980,30 +1004,6 @@
Contributing
marker_right.bindPopup("Adam Layne
GitHub: fNBU"); markers.addLayer(marker_right); -var marker = L.marker([20.173226, 85.684102]); -marker.bindPopup("Abhijit Chakraborty
GitHub: Abhijit-niser"); -markers.addLayer(marker); - -var marker_left = L.marker([20.173226, -274.315898]); -marker_left.bindPopup("Abhijit Chakraborty
GitHub: Abhijit-niser"); -markers.addLayer(marker_left); - -var marker_right = L.marker([20.173226, 445.684102]); -marker_right.bindPopup("Abhijit Chakraborty
GitHub: Abhijit-niser"); -markers.addLayer(marker_right); - -var marker = L.marker([37.55, -121.99]); -marker.bindPopup("Anirudh Rao
GitHub: rao107"); -markers.addLayer(marker); - -var marker_left = L.marker([37.55, -481.99]); -marker_left.bindPopup("Anirudh Rao
GitHub: rao107"); -markers.addLayer(marker_left); - -var marker_right = L.marker([37.55, 238.01]); -marker_right.bindPopup("Anirudh Rao
GitHub: rao107"); -markers.addLayer(marker_right); - var marker = L.marker([44.83, -0.57]); marker.bindPopup("Philippe Duchon"); markers.addLayer(marker); @@ -2036,15 +2036,15 @@
Contributing
marker_right.bindPopup("Oliver Butterley
GitHub: oliver-butterley"); markers.addLayer(marker_right); -var marker = L.marker([50.728899, 7.083816]); +var marker = L.marker([50.728052, 7.083389]); marker.bindPopup("Floris van Doorn
GitHub: fpvandoorn"); markers.addLayer(marker); -var marker_left = L.marker([50.728899, -352.916184]); +var marker_left = L.marker([50.728052, -352.916611]); marker_left.bindPopup("Floris van Doorn
GitHub: fpvandoorn"); markers.addLayer(marker_left); -var marker_right = L.marker([50.728899, 367.083816]); +var marker_right = L.marker([50.728052, 367.083389]); marker_right.bindPopup("Floris van Doorn
GitHub: fpvandoorn"); markers.addLayer(marker_right);