diff --git a/Zeta3Irrational.lean b/Zeta3Irrational.lean index c779005..5298524 100644 --- a/Zeta3Irrational.lean +++ b/Zeta3Irrational.lean @@ -1,7 +1,8 @@ import Zeta3Irrational.Basic import Zeta3Irrational.Bound -import Zeta3Irrational.Equality import Zeta3Irrational.Integral import Zeta3Irrational.LegendrePoly import Zeta3Irrational.LinearForm import Zeta3Irrational.d +import Zeta3Irrational.Equality +import Zeta3Irrational.PrimeCounting diff --git a/Zeta3Irrational/Basic.lean b/Zeta3Irrational/Basic.lean index 3583719..8014ec5 100644 --- a/Zeta3Irrational/Basic.lean +++ b/Zeta3Irrational/Basic.lean @@ -2,42 +2,49 @@ A formal proof of the irrationality of Riemann-Zeta(3). Author: Junqi Liu and Jujian Zhang. -/ -import Mathlib.Data.Int.Star import Mathlib.NumberTheory.LSeries.HurwitzZetaValues -import Mathlib.Order.CompletePartialOrder -import Mathlib.RingTheory.DedekindDomain.Dvr -import PrimeNumberTheoremAnd.Consequences +import Zeta3Irrational.PrimeCounting import Zeta3Irrational.Bound import Zeta3Irrational.LegendrePoly import Zeta3Irrational.LinearForm +/-! # Apéry's irrationality proof for ζ(3) + +Port of the Apache-2.0 source by Junqi Liu and Jujian Zhang. +-/ + open scoped Nat open BigOperators Polynomial +/-- The logarithmic double integral weighted by two real shifted Legendre polynomials. -/ noncomputable abbrev JJ (n : ℕ) : ℝ := ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, - (-(x.1 * x.2).log / (1 - x.1 * x.2) * (shiftedLegendre n).eval x.1 * (shiftedLegendre n).eval x.2) + (-(x.1 * x.2).log / (1 - x.1 * x.2) * (aperyShiftedLegendre n).eval x.1 * + (aperyShiftedLegendre n).eval x.2) +/-- The equivalent positive triple integral in the Apéry identity. -/ noncomputable abbrev JJ' (n : ℕ) : ℝ := ∫ (x : ℝ × ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, (x.2.1 * (1 - x.2.1) * x.2.2 * (1 - x.2.2) * x.1 * (1 - x.1) / (1 - (1 - x.2.1 * x.2.2) * x.1)) ^ n / (1 - (1 - x.2.1 * x.2.2) * x.1) +/-- The nonnegative extended-real integral of the positive Apéry integrand. -/ noncomputable abbrev JJENN (n : ℕ) : ENNReal := ∫⁻ (x : ℝ × ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, ENNReal.ofReal ((x.2.1 * (1 - x.2.1) * x.2.2 * (1 - x.2.2) * x.1 * (1 - x.1) / (1 - (1 - x.2.1 * x.2.2) * x.1)) ^ n / (1 - (1 - x.2.1 * x.2.2) * x.1)) +/-- The Apéry double integral multiplied by the cube of the least common multiple. -/ noncomputable abbrev fun1 (n : ℕ) : ℝ := (d (Finset.Icc 1 n)) ^ 3 * JJ n theorem linear_int (n : ℕ) : ∃ a b : ℕ → ℤ, fun1 n = a n + b n * (d (Finset.Icc 1 n) : ℤ) ^ 3 * ∑' n : ℕ , 1 / ((n : ℝ) + 1) ^ 3 := by delta fun1 JJ obtain ⟨c, hc⟩ := shiftedLegendre_eq_int_poly n - simp_rw [hc, Polynomial.eval_finset_sum, mul_assoc, Finset.sum_mul_sum, Finset.mul_sum] - simp only [zsmul_eq_mul, eval_mul, eval_intCast, eval_pow, eval_X] + simp_rw [hc, Polynomial.eval_finsetSum, mul_assoc, Finset.sum_mul_sum, Finset.mul_sum] + simp only [eval_mul, eval_intCast, eval_pow, eval_X] simp_rw [← mul_assoc, multi_integral_sum_comm, multi_integral_mul_const] - simp only [← Finset.sum_neg_distrib, Finset.mul_sum] + simp only [Finset.mul_sum] obtain ⟨qq', ⟨pp', hqq'⟩⟩ := linear_int_aux use fun n => ∑ x ∈ Finset.range (n + 1), ∑ i ∈ Finset.range (n + 1), d (Finset.Icc 1 n) ^ 3 * c x * c i * qq' x i / d (Finset.Icc 1 (Nat.max x i)) ^ 3 @@ -70,10 +77,10 @@ theorem linear_int (n : ℕ) : ∃ a b : ℕ → ℤ, simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, IsIntegrallyClosed.pow_dvd_pow_iff] norm_cast apply d_dvd_d_of_le - simp_all only [zsmul_eq_mul, Finset.mem_range, Finset.le_eq_subset] + simp_all only [Finset.mem_range] intro a b simp_all only [Finset.mem_Icc, true_and] - simp only [one_div, le_max_iff] at b + simp only [le_max_iff] at b rcases b with ⟨_ ,(c | c)⟩ <;> linarith @@ -83,7 +90,8 @@ theorem linear_int (n : ℕ) : ∃ a b : ℕ → ℤ, simp · ring -lemma pos_aux (x : ℝ × ℝ × ℝ) (hx : (0 < x.1 ∧ x.1 < 1) ∧ (0 < x.2.1 ∧ x.2.1 < 1) ∧ 0 < x.2.2 ∧ x.2.2 < 1) : +lemma pos_aux (x : ℝ × ℝ × ℝ) (hx : (0 < x.1 ∧ x.1 < 1) ∧ (0 < x.2.1 ∧ x.2.1 < 1) ∧ 0 < x.2.2 ∧ + x.2.2 < 1) : 0 < (1 - (1 - x.2.1 * x.2.2) * x.1) := by simp only [sub_pos] suffices (1 - x.2.1 * x.2.2) * x.1 < x.1 by linarith @@ -120,7 +128,8 @@ lemma JJENN_upper (n : ℕ) : JJENN n ≤ apply bound' <;> linarith · exact pos_aux x h · simp only [h, ↓reduceIte, le_refl] - _ = ENNReal.ofReal ((1 / 24) ^ n) * ∫⁻ (x : ℝ × ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, + _ = ENNReal.ofReal ((1 / 24) ^ n) * ∫⁻ (x : ℝ × ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 ×ˢ + Set.Ioo 0 1, ENNReal.ofReal (1 / (1 - (1 - x.2.1 * x.2.2) * x.1)) := by rw [← MeasureTheory.lintegral_const_mul] · rw [← MeasureTheory.lintegral_indicator (by measurability), @@ -139,8 +148,8 @@ lemma JJENN_upper (n : ℕ) : JJENN n ≤ apply Measurable.mul _ measurable_fst apply Measurable.const_sub apply Measurable.mul - apply Measurable.comp' measurable_fst measurable_snd - apply Measurable.comp' measurable_snd measurable_snd + · exact measurable_fst.comp measurable_snd + · exact measurable_snd.comp measurable_snd _ = ENNReal.ofReal (2 * (1 / 24) ^ n * ∑' n : ℕ , 1 / ((n : ℝ) + 1) ^ 3) := by have h := JENN_eq_triple 0 0 simp only [pow_zero, mul_one] at h @@ -151,40 +160,14 @@ lemma JJENN_upper (n : ℕ) : JJENN n ≤ nth_rw 2 [mul_comm] lemma integrableOn_JJ' (n : ℕ) : MeasureTheory.Integrable (fun (x : ℝ × ℝ × ℝ) ↦ - (x.2.1 * (1 - x.2.1) * x.2.2 * (1 - x.2.2) * x.1 * (1 - x.1) / (1 - (1 - x.2.1 * x.2.2) * x.1)) ^ n / - (1 - (1 - x.2.1 * x.2.2) * x.1)) (MeasureTheory.volume.restrict (Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1)) := by + (x.2.1 * (1 - x.2.1) * x.2.2 * (1 - x.2.2) * x.1 * (1 - x.1) / (1 - (1 - x.2.1 * x.2.2) * + x.1)) ^ n / + (1 - (1 - x.2.1 * x.2.2) * x.1)) (MeasureTheory.volume.restrict (Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 + ×ˢ Set.Ioo 0 1)) := by rw [MeasureTheory.Integrable] constructor - · apply AEMeasurable.aestronglyMeasurable - rw [← aemeasurable_indicator_iff (by measurability)] - apply AEMeasurable.indicator _ (by measurability) - apply AEMeasurable.div - · apply AEMeasurable.pow_const - apply AEMeasurable.div - · apply AEMeasurable.mul _ (AEMeasurable.const_sub (AEMeasurable.fst (f := id) aemeasurable_id) _) - apply AEMeasurable.mul _ (AEMeasurable.fst (f := id) aemeasurable_id) - apply AEMeasurable.mul _ (AEMeasurable.const_sub (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.2) - (AEMeasurable.snd (f := id) aemeasurable_id)) _) - apply AEMeasurable.mul _ (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.2) - (AEMeasurable.snd (f := id) aemeasurable_id)) - apply AEMeasurable.mul _ (AEMeasurable.const_sub (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.1) - (AEMeasurable.fst (f := id) aemeasurable_id)) _) - exact (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.1) - (AEMeasurable.fst (f := id) aemeasurable_id)) - · apply AEMeasurable.const_sub - apply AEMeasurable.mul _ (AEMeasurable.fst (f := id) aemeasurable_id) - apply AEMeasurable.const_sub - apply AEMeasurable.mul _ (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.2) - (AEMeasurable.snd (f := id) aemeasurable_id)) - exact (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.1) - (AEMeasurable.fst (f := id) aemeasurable_id)) - · apply AEMeasurable.const_sub - apply AEMeasurable.mul _ (AEMeasurable.fst (f := id) aemeasurable_id) - apply AEMeasurable.const_sub - apply AEMeasurable.mul _ (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.2) - (AEMeasurable.snd (f := id) aemeasurable_id)) - exact (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.1) - (AEMeasurable.fst (f := id) aemeasurable_id)) + · apply Measurable.aestronglyMeasurable + fun_prop · rw [MeasureTheory.hasFiniteIntegral_iff_norm] set k := _ change k < ⊤ @@ -196,16 +179,16 @@ lemma integrableOn_JJ' (n : ℕ) : MeasureTheory.Integrable (fun (x : ℝ × ℝ ext x rw [Set.indicator_apply, Set.indicator_apply] by_cases hx : x ∈ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 - · simp only [hx, ↓reduceIte, norm_mul, norm_div, norm_neg, Real.norm_eq_abs, norm_pow] + · simp only [hx, ↓reduceIte, norm_mul, norm_div, Real.norm_eq_abs, norm_pow] simp only [Set.mem_prod, Set.mem_Ioo] at hx rw [ENNReal.ofReal_eq_ofReal_iff] · congr 3 · rw [abs_eq_self.2, abs_eq_self.2, abs_eq_self.2, abs_eq_self.2, abs_eq_self.2, abs_eq_self.2] <;> nlinarith · simp only [abs_eq_self, sub_nonneg] - apply mul_le_one₀ (by nlinarith) (by linarith) (by linarith) + exact (mul_le_of_le_one_left (by linarith) (by nlinarith)).trans (by linarith) · simp only [abs_eq_self, sub_nonneg] - apply mul_le_one₀ (by nlinarith) (by linarith) (by linarith) + exact (mul_le_of_le_one_left (by linarith) (by nlinarith)).trans (by linarith) · positivity · apply div_nonneg · apply pow_nonneg @@ -223,13 +206,14 @@ lemma integrableOn_JJ' (n : ℕ) : MeasureTheory.Integrable (fun (x : ℝ × ℝ simp only [one_div, inv_pow, ENNReal.ofReal_lt_top] lemma shiftedLegendre_bound (n : ℕ) (x : ℝ) (hx : 0 < x ∧ x < 1) : - |eval x (shiftedLegendre n)| ≤ ∑ x_1 ∈ Finset.range (n + 1), (n.choose x_1 : ℝ) * ((n + x_1).choose n) := by - simp only [shiftedLegendre_eq_sum, map_pow, map_neg, map_one, smul_eq_mul, eval_finset_sum, + |eval x (aperyShiftedLegendre n)| ≤ ∑ x_1 ∈ Finset.range (n + 1), (n.choose x_1 : ℝ) * ((n + + x_1).choose n) := by + simp only [shiftedLegendre_eq_sum, map_pow, map_neg, map_one, eval_finsetSum, eval_mul, eval_pow, eval_neg, eval_one, eval_natCast, eval_X] - have := Finset.abs_sum_le_sum_abs (f := fun y => (-1) ^ y * ↑(n.choose y) * ↑((n + y).choose n) * x ^ y) + have := Finset.abs_sum_le_sum_abs (f := fun y => (-1) ^ y * ↑(n.choose y) * ↑((n + y).choose + n) * x ^ y) (s := Finset.range (n + 1)) - trans - apply this + refine this.trans ?_ apply Finset.sum_le_sum intro i _ simp only [abs_mul, abs_pow, abs_neg, abs_one, one_pow, Nat.abs_cast, one_mul] @@ -243,51 +227,24 @@ lemma shiftedLegendre_bound (n : ℕ) (x : ℝ) (hx : 0 < x ∧ x < 1) : lemma Measurable_one_div_aux : Measurable fun (x : ℝ × ℝ × ℝ) ↦ ENNReal.ofReal (1 / (1 - (1 - x.2.1 * x.2.2) * x.1)) := by - apply Measurable.ennreal_ofReal - apply Measurable.const_div - apply Measurable.const_sub - apply Measurable.mul _ measurable_fst - apply Measurable.const_sub - apply Measurable.mul - apply Measurable.comp' measurable_fst measurable_snd - apply Measurable.comp' measurable_snd measurable_snd + fun_prop lemma integrableOn_JJ1 (n : ℕ) : MeasureTheory.Integrable - (Function.uncurry fun z x ↦ eval x.1 (shiftedLegendre n) * eval x.2 (shiftedLegendre n) * (1 / (1 - (1 - x.1 * x.2) * z))) - ((MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo 0 1 ×ˢ Set.Ioo 0 1))) := by - rw [MeasureTheory.Measure.prod_restrict, ← MeasureTheory.Measure.volume_eq_prod, MeasureTheory.Integrable] + (Function.uncurry fun z x ↦ eval x.1 (aperyShiftedLegendre n) * eval x.2 + (aperyShiftedLegendre n) * (1 / (1 - (1 - x.1 * x.2) * z))) + ((MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo 0 + 1 ×ˢ Set.Ioo 0 1))) := by + rw [MeasureTheory.Measure.prod_restrict, ← MeasureTheory.Measure.volume_eq_prod, + MeasureTheory.Integrable] constructor - · apply AEMeasurable.aestronglyMeasurable - rw [← aemeasurable_indicator_iff (by measurability)] - apply AEMeasurable.indicator _ (by measurability) - simp_rw [mul_one_div] - apply AEMeasurable.div - · simp only [shiftedLegendre_eq_sum, map_pow, map_neg, map_one, smul_eq_mul] - apply AEMeasurable.mul - · simp only [eval_finset_sum, eval_mul, eval_pow, eval_neg, eval_one, eval_natCast, eval_X] - apply Finset.aemeasurable_sum - intro i _ - apply AEMeasurable.const_mul - apply AEMeasurable.pow_const (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.1) _) - apply AEMeasurable.fst (f := id) aemeasurable_id - · simp only [eval_finset_sum, eval_mul, eval_pow, eval_neg, eval_one, eval_natCast, eval_X] - apply Finset.aemeasurable_sum - intro i _ - apply AEMeasurable.const_mul - apply AEMeasurable.pow_const (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.2) _) - apply AEMeasurable.snd (f := id) aemeasurable_id - · apply AEMeasurable.const_sub - apply AEMeasurable.mul _ (AEMeasurable.fst (f := id) aemeasurable_id) - apply AEMeasurable.const_sub - apply AEMeasurable.mul _ (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.2) - (AEMeasurable.snd (f := id) aemeasurable_id)) - exact (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.1) - (AEMeasurable.fst (f := id) aemeasurable_id)) + · apply Measurable.aestronglyMeasurable + fun_prop · rw [MeasureTheory.hasFiniteIntegral_iff_norm] set k := _ set C := ∑ x_1 ∈ Finset.range (n + 1), (n.choose x_1 : ℝ) * ((n + x_1).choose n) change k < ⊤ - have : k ≤ ENNReal.ofReal (C ^ 2) * ∫⁻ (x : ℝ × ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, + have : k ≤ ENNReal.ofReal (C ^ 2) * ∫⁻ (x : ℝ × ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 ×ˢ + Set.Ioo 0 1, ENNReal.ofReal (1 / (1 - (1 - x.2.1 * x.2.2) * x.1)) := by simp only [k] rw [← MeasureTheory.lintegral_const_mul _ Measurable_one_div_aux] @@ -323,46 +280,21 @@ lemma integrableOn_JJ1 (n : ℕ) : MeasureTheory.Integrable · positivity lemma integrableOn_JJ2 (n : ℕ) : MeasureTheory.Integrable (Function.uncurry fun z x ↦ - eval x.1 (shiftedLegendre n) * (x.1 * x.2 * z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z) ^ (n + 1)) - ((MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo 0 1 ×ˢ Set.Ioo 0 1))) := by - rw [MeasureTheory.Measure.prod_restrict, ← MeasureTheory.Measure.volume_eq_prod, MeasureTheory.Integrable] + eval x.1 (aperyShiftedLegendre n) * (x.1 * x.2 * z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * + x.2) * z) ^ (n + 1)) + ((MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo 0 + 1 ×ˢ Set.Ioo 0 1))) := by + rw [MeasureTheory.Measure.prod_restrict, ← MeasureTheory.Measure.volume_eq_prod, + MeasureTheory.Integrable] constructor - · apply AEMeasurable.aestronglyMeasurable - rw [← aemeasurable_indicator_iff (by measurability)] - apply AEMeasurable.indicator _ (by measurability) - apply AEMeasurable.div - · simp only [shiftedLegendre_eq_sum, map_pow, map_neg, map_one, smul_eq_mul] - apply AEMeasurable.mul - · apply AEMeasurable.mul - · simp only [eval_finset_sum, eval_mul, eval_pow, eval_neg, eval_one, eval_natCast, eval_X] - apply Finset.aemeasurable_sum - intro i _ - apply AEMeasurable.const_mul - apply AEMeasurable.pow_const (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.1) _) - apply AEMeasurable.fst (f := id) aemeasurable_id - · apply AEMeasurable.pow_const - apply AEMeasurable.mul _ (AEMeasurable.fst (f := id) aemeasurable_id) - apply AEMeasurable.mul _ (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.2) - (AEMeasurable.snd (f := id) aemeasurable_id)) - apply AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.1) - apply AEMeasurable.fst (f := id) aemeasurable_id - · apply AEMeasurable.pow_const - apply AEMeasurable.const_sub - apply AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.2) - (AEMeasurable.snd (f := id) aemeasurable_id) - · apply AEMeasurable.pow_const - apply AEMeasurable.const_sub - apply AEMeasurable.mul _ (AEMeasurable.fst (f := id) aemeasurable_id) - apply AEMeasurable.const_sub - apply AEMeasurable.mul _ (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.2) - (AEMeasurable.snd (f := id) aemeasurable_id)) - apply AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.1) - apply AEMeasurable.fst (f := id) aemeasurable_id + · apply Measurable.aestronglyMeasurable + fun_prop · rw [MeasureTheory.hasFiniteIntegral_iff_norm] set k := _ set C := ∑ x_1 ∈ Finset.range (n + 1), (n.choose x_1 : ℝ) * ((n + x_1).choose n) change k < ⊤ - have : k ≤ ENNReal.ofReal (|C|) * ∫⁻ (x : ℝ × ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, + have : k ≤ ENNReal.ofReal (|C|) * ∫⁻ (x : ℝ × ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 ×ˢ + Set.Ioo 0 1, ENNReal.ofReal (1 / (1 - (1 - x.2.1 * x.2.2) * x.1)) := by simp only [k] rw [← MeasureTheory.lintegral_const_mul _ Measurable_one_div_aux] @@ -376,7 +308,8 @@ lemma integrableOn_JJ2 (n : ℕ) : MeasureTheory.Integrable (Function.uncurry fu simp only [Set.mem_prod, Set.mem_Ioo] at hx rw [← ENNReal.ofReal_mul] · rw [ENNReal.ofReal_le_ofReal_iff] - · rw [Function.uncurry_apply_pair, pow_add, ← div_div, abs_div,mul_one_div, div_le_div_iff₀] + · rw [Function.uncurry_apply_pair, pow_add, ← div_div, abs_div,mul_one_div, + div_le_div_iff₀] · apply mul_le_mul _ _ (by linarith [pos_aux x hx]) (by positivity) · rw [← mul_div, mul_assoc, abs_mul, ← mul_one (a := |C|)] apply mul_le_mul _ _ (by positivity) (by positivity) @@ -406,16 +339,10 @@ lemma integrableOn_JJ2 (n : ℕ) : MeasureTheory.Integrable (Function.uncurry fu · linarith · linarith · exact ineq - · rw [div_add_one] + · rw [div_add_one (by positivity)] intro r rw [_root_.div_eq_zero_iff] at r - · refine ineq <| r.resolve_right ?_ - apply mul_ne_zero - · apply mul_ne_zero <;> linarith - · linarith - · apply mul_ne_zero - · apply mul_ne_zero <;> linarith - · linarith, abs_div] + exact ineq (r.resolve_right (by positivity)), abs_div] trans |1 - z| · apply div_le_self (abs_nonneg _) rw [abs_of_nonneg, le_add_iff_nonneg_left] @@ -446,46 +373,25 @@ lemma integrableOn_JJ2 (n : ℕ) : MeasureTheory.Integrable (Function.uncurry fu have h := JENN_eq_triple 0 0 simp only [pow_zero, mul_one] at h rw [← h, J_ENN_rr, ← ENNReal.ofReal_mul] - · simp + · finiteness · positivity lemma integrableOn_JJ3 (n : ℕ) : MeasureTheory.Integrable - (Function.uncurry fun z x ↦ eval x.1 (shiftedLegendre n) * (1 - z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z)) - ((MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo 0 1 ×ˢ Set.Ioo 0 1))) := by - rw [MeasureTheory.Measure.prod_restrict, ← MeasureTheory.Measure.volume_eq_prod, MeasureTheory.Integrable] + (Function.uncurry fun z x ↦ eval x.1 (aperyShiftedLegendre n) * (1 - z) ^ n * (1 - x.2) ^ n / + (1 - (1 - x.1 * x.2) * z)) + ((MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo 0 + 1 ×ˢ Set.Ioo 0 1))) := by + rw [MeasureTheory.Measure.prod_restrict, ← MeasureTheory.Measure.volume_eq_prod, + MeasureTheory.Integrable] constructor - · apply AEMeasurable.aestronglyMeasurable - rw [← aemeasurable_indicator_iff (by measurability)] - apply AEMeasurable.indicator _ (by measurability) - apply AEMeasurable.div - · simp only [shiftedLegendre_eq_sum, map_pow, map_neg, map_one, smul_eq_mul] - apply AEMeasurable.mul - · apply AEMeasurable.mul - · simp only [eval_finset_sum, eval_mul, eval_pow, eval_neg, eval_one, eval_natCast, eval_X] - apply Finset.aemeasurable_sum - intro i _ - apply AEMeasurable.const_mul - apply AEMeasurable.pow_const (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.1) _) - apply AEMeasurable.fst (f := id) aemeasurable_id - · apply AEMeasurable.pow_const - apply AEMeasurable.const_sub - apply AEMeasurable.fst (f := id) aemeasurable_id - · apply AEMeasurable.pow_const - apply AEMeasurable.const_sub - apply AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.2) - (AEMeasurable.snd (f := id) aemeasurable_id) - · apply AEMeasurable.const_sub - apply AEMeasurable.mul _ (AEMeasurable.fst (f := id) aemeasurable_id) - apply AEMeasurable.const_sub - apply AEMeasurable.mul _ (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.2) - (AEMeasurable.snd (f := id) aemeasurable_id)) - apply AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.1) - apply AEMeasurable.fst (f := id) aemeasurable_id + · apply Measurable.aestronglyMeasurable + fun_prop · rw [MeasureTheory.hasFiniteIntegral_iff_norm] set k := _ set C := ∑ x_1 ∈ Finset.range (n + 1), (n.choose x_1 : ℝ) * ((n + x_1).choose n) change k < ⊤ - have : k ≤ ENNReal.ofReal (|C|) * ∫⁻ (x : ℝ × ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, + have : k ≤ ENNReal.ofReal (|C|) * ∫⁻ (x : ℝ × ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 ×ˢ + Set.Ioo 0 1, ENNReal.ofReal (1 / (1 - (1 - x.2.1 * x.2.2) * x.1)) := by simp only [k] rw [← MeasureTheory.lintegral_const_mul _ Measurable_one_div_aux] @@ -532,37 +438,78 @@ lemma integrableOn_JJ3 (n : ℕ) : MeasureTheory.Integrable have h := JENN_eq_triple 0 0 simp only [pow_zero, mul_one] at h rw [← h, J_ENN_rr, ← ENNReal.ofReal_mul] - · simp + · finiteness · positivity lemma eq1_integrableOn_aux1 (n : ℕ) (z : ℝ) (hz : z ∈ Set.Ioo 0 1) : MeasureTheory.Integrable - (fun x ↦ eval x.1 (shiftedLegendre n) * eval x.2 (shiftedLegendre n) * (1 / (1 - (1 - x.1 * x.2) * z))) - ((MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo 0 1))) := by + (fun x ↦ eval x.1 (aperyShiftedLegendre n) * eval x.2 (aperyShiftedLegendre n) * (1 / (1 - + (1 - x.1 * x.2) * z))) + ((MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo + 0 1))) := by rw [MeasureTheory.Measure.prod_restrict, ← MeasureTheory.Measure.volume_eq_prod] apply MeasureTheory.IntegrableOn.integrable apply MeasureTheory.IntegrableOn.mono_set (t := Set.Icc 0 1 ×ˢ Set.Icc 0 1) - apply ContinuousOn.integrableOn_compact - · simp only [Set.mem_Ioo, Set.Icc_prod_Icc, Prod.mk_zero_zero, Prod.mk_one_one,isCompact_Icc] - · simp only [shiftedLegendre_eq_sum, map_pow, map_neg, map_one, smul_eq_mul] - apply ContinuousOn.mul - · apply ContinuousOn.mul - · simp only [eval_finset_sum, eval_mul, eval_pow, eval_neg, eval_one, eval_natCast, eval_X] - apply continuousOn_finset_sum - intro i _ - apply ContinuousOn.mul continuousOn_const - apply ContinuousOn.pow continuousOn_fst - · simp only [eval_finset_sum, eval_mul, eval_pow, eval_neg, eval_one, eval_natCast, eval_X] - apply continuousOn_finset_sum - intro i _ - apply ContinuousOn.mul continuousOn_const - apply ContinuousOn.pow continuousOn_snd - · apply ContinuousOn.div continuousOn_const - · apply ContinuousOn.sub continuousOn_const + · apply ContinuousOn.integrableOn_compact + · simp only [Set.Icc_prod_Icc, Prod.mk_zero_zero, Prod.mk_one_one,isCompact_Icc] + · simp only [shiftedLegendre_eq_sum, map_pow, map_neg, map_one] + apply ContinuousOn.mul + · apply ContinuousOn.mul + · simp only [eval_finsetSum, eval_mul, eval_pow, eval_neg, eval_one, eval_natCast, eval_X] + apply continuousOn_finsetSum + intro i _ + apply ContinuousOn.mul continuousOn_const + apply ContinuousOn.pow continuousOn_fst + · simp only [eval_finsetSum, eval_mul, eval_pow, eval_neg, eval_one, eval_natCast, eval_X] + apply continuousOn_finsetSum + intro i _ + apply ContinuousOn.mul continuousOn_const + apply ContinuousOn.pow continuousOn_snd + · apply ContinuousOn.div continuousOn_const + · apply ContinuousOn.sub continuousOn_const + apply ContinuousOn.mul _ continuousOn_const + apply ContinuousOn.sub continuousOn_const + apply ContinuousOn.mul continuousOn_fst continuousOn_snd + · intro x hx + suffices 1 - (1 - x.1 * x.2) * z > 0 by linarith + simp only [Set.mem_prod, Set.mem_Icc] at hx + simp only [Set.mem_Ioo, gt_iff_lt, sub_pos] at hz ⊢ + suffices (1 - x.1 * x.2) * z ≤ z by linarith + apply mul_le_of_le_one_left (by linarith) + simp only [tsub_le_iff_right, le_add_iff_nonneg_right] + nlinarith + · apply Set.prod_mono Set.Ioo_subset_Icc_self Set.Ioo_subset_Icc_self + +lemma eq1_integrableOn_aux2 (n : ℕ) (z : ℝ) (hz : z ∈ Set.Ioo 0 1) : MeasureTheory.Integrable + (fun x ↦ eval x.1 (aperyShiftedLegendre n) * (x.1 * x.2 * z) ^ n * (1 - x.2) ^ n / (1 - (1 + - x.1 * x.2) * z) ^ (n + 1)) + ((MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo + 0 1))) := by + rw [MeasureTheory.Measure.prod_restrict, ← MeasureTheory.Measure.volume_eq_prod] + apply MeasureTheory.IntegrableOn.integrable + apply MeasureTheory.IntegrableOn.mono_set (t := Set.Icc 0 1 ×ˢ Set.Icc 0 1) + · apply ContinuousOn.integrableOn_compact + · simp only [Set.Icc_prod_Icc, Prod.mk_zero_zero, Prod.mk_one_one,isCompact_Icc] + · simp only [shiftedLegendre_eq_sum, map_pow, map_neg, map_one] + apply ContinuousOn.div + · apply ContinuousOn.mul + · apply ContinuousOn.mul + · simp only [eval_finsetSum, eval_mul, eval_pow, eval_neg, eval_one, eval_natCast, eval_X] + apply continuousOn_finsetSum + intro i _ + apply ContinuousOn.mul continuousOn_const + apply ContinuousOn.pow continuousOn_fst + · apply ContinuousOn.pow + apply ContinuousOn.mul _ continuousOn_const + apply ContinuousOn.mul continuousOn_fst continuousOn_snd + · apply ContinuousOn.pow + apply ContinuousOn.sub continuousOn_const continuousOn_snd + · apply ContinuousOn.pow + apply ContinuousOn.sub continuousOn_const apply ContinuousOn.mul _ continuousOn_const apply ContinuousOn.sub continuousOn_const apply ContinuousOn.mul continuousOn_fst continuousOn_snd · intro x hx - suffices 1 - (1 - x.1 * x.2) * z > 0 by linarith + suffices 1 - (1 - x.1 * x.2) * z > 0 by positivity simp only [Set.mem_prod, Set.mem_Icc] at hx simp only [Set.mem_Ioo, gt_iff_lt, sub_pos] at hz ⊢ suffices (1 - x.1 * x.2) * z ≤ z by linarith @@ -571,88 +518,62 @@ lemma eq1_integrableOn_aux1 (n : ℕ) (z : ℝ) (hz : z ∈ Set.Ioo 0 1) : Measu nlinarith · apply Set.prod_mono Set.Ioo_subset_Icc_self Set.Ioo_subset_Icc_self -lemma eq1_integrableOn_aux2 (n : ℕ) (z : ℝ) (hz : z ∈ Set.Ioo 0 1) : MeasureTheory.Integrable - (fun x ↦ eval x.1 (shiftedLegendre n) * (x.1 * x.2 * z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z) ^ (n + 1)) - ((MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo 0 1))) := by - rw [MeasureTheory.Measure.prod_restrict, ← MeasureTheory.Measure.volume_eq_prod] - apply MeasureTheory.IntegrableOn.integrable - apply MeasureTheory.IntegrableOn.mono_set (t := Set.Icc 0 1 ×ˢ Set.Icc 0 1) - apply ContinuousOn.integrableOn_compact - · simp only [Set.mem_Ioo, Set.Icc_prod_Icc, Prod.mk_zero_zero, Prod.mk_one_one,isCompact_Icc] - · simp only [shiftedLegendre_eq_sum, map_pow, map_neg, map_one, smul_eq_mul] - apply ContinuousOn.div - · apply ContinuousOn.mul - · apply ContinuousOn.mul - · simp only [eval_finset_sum, eval_mul, eval_pow, eval_neg, eval_one, eval_natCast, eval_X] - apply continuousOn_finset_sum - intro i _ - apply ContinuousOn.mul continuousOn_const - apply ContinuousOn.pow continuousOn_fst - · apply ContinuousOn.pow - apply ContinuousOn.mul _ continuousOn_const - apply ContinuousOn.mul continuousOn_fst continuousOn_snd - · apply ContinuousOn.pow - apply ContinuousOn.sub continuousOn_const continuousOn_snd - · apply ContinuousOn.pow - apply ContinuousOn.sub continuousOn_const - apply ContinuousOn.mul _ continuousOn_const - apply ContinuousOn.sub continuousOn_const - apply ContinuousOn.mul continuousOn_fst continuousOn_snd - · intro x hx - suffices 1 - (1 - x.1 * x.2) * z > 0 by positivity - simp only [Set.mem_prod, Set.mem_Icc] at hx - simp only [Set.mem_Ioo, gt_iff_lt, sub_pos] at hz ⊢ - suffices (1 - x.1 * x.2) * z ≤ z by linarith - apply mul_le_of_le_one_left (by linarith) - simp only [tsub_le_iff_right, le_add_iff_nonneg_right] - nlinarith - · apply Set.prod_mono Set.Ioo_subset_Icc_self Set.Ioo_subset_Icc_self - -lemma double_integral_eq1 (n : ℕ) (z : ℝ) (hz : z ∈ Set.Ioo 0 1) : ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, - eval x.1 (shiftedLegendre n) * eval x.2 (shiftedLegendre n) * (1 / (1 - (1 - x.1 * x.2) * z)) = +lemma double_integral_eq1 (n : ℕ) (z : ℝ) (hz : z ∈ Set.Ioo 0 1) : ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 + ×ˢ Set.Ioo 0 1, + eval x.1 (aperyShiftedLegendre n) * eval x.2 (aperyShiftedLegendre n) * (1 / (1 - (1 - x.1 + * x.2) * z)) = ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, - eval x.1 (shiftedLegendre n) * (x.1 * x.2 * z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z) ^ (n + 1) := by + eval x.1 (aperyShiftedLegendre n) * (x.1 * x.2 * z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * + x.2) * z) ^ (n + 1) := by calc - _ = ∫ (x : ℝ) in Set.Ioo 0 1, eval x (shiftedLegendre n) * ∫ (y : ℝ) in Set.Ioo 0 1, - eval y (shiftedLegendre n) * (1 / (1 - (1 - x * y) * z)) := by + _ = ∫ (x : ℝ) in Set.Ioo 0 1, eval x (aperyShiftedLegendre n) * ∫ (y : ℝ) in Set.Ioo 0 1, + eval y (aperyShiftedLegendre n) * (1 / (1 - (1 - x * y) * z)) := by rw [MeasureTheory.Measure.volume_eq_prod, ← MeasureTheory.Measure.prod_restrict, MeasureTheory.integral_prod] · apply MeasureTheory.setIntegral_congr_fun (by measurability) intro x _ simp only - rw [← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by norm_num), - ← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by norm_num), + rw [← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by + norm_num), + ← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by + norm_num), ← intervalIntegral.integral_const_mul] simp only [one_div, ← mul_assoc] · exact eq1_integrableOn_aux1 n z hz - _ = ∫ (x : ℝ) in Set.Ioo 0 1, eval x (shiftedLegendre n) * ∫ (y : ℝ) in Set.Ioo 0 1, + _ = ∫ (x : ℝ) in Set.Ioo 0 1, eval x (aperyShiftedLegendre n) * ∫ (y : ℝ) in Set.Ioo 0 1, (x * y * z) ^ n * (1 - y) ^ n / (1 - (1 - x * y) * z) ^ (n + 1) := by apply MeasureTheory.setIntegral_congr_fun (by measurability) intro x hx simp only congr 1 - rw [← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by norm_num), - ← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by norm_num)] + rw [← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by + norm_num), + ← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by + norm_num)] rw [legendre_integral_special n hx hz] _ = ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, - eval x.1 (shiftedLegendre n) * (x.1 * x.2 * z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z) ^ (n + 1) := by + eval x.1 (aperyShiftedLegendre n) * (x.1 * x.2 * z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * + x.2) * z) ^ (n + 1) := by rw [MeasureTheory.Measure.volume_eq_prod, ← MeasureTheory.Measure.prod_restrict, MeasureTheory.integral_prod] · apply MeasureTheory.setIntegral_congr_fun (by measurability) intro x _ simp only - rw [← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by norm_num), - ← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by norm_num), + rw [← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by + norm_num), + ← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by + norm_num), ← intervalIntegral.integral_const_mul] simp only [mul_div, ← mul_assoc] · exact eq1_integrableOn_aux2 n z hz -lemma ineq_aux (x : ℝ × ℝ) (z : ℝ) (hx : (0 < x.1 ∧ x.1 < 1) ∧ 0 < x.2 ∧ x.2 < 1) (hz : 0 ≤ z ∧ z ≤ 1) : +lemma ineq_aux (x : ℝ × ℝ) (z : ℝ) (hx : (0 < x.1 ∧ x.1 < 1) ∧ 0 < x.2 ∧ x.2 < 1) (hz : 0 ≤ z ∧ + z ≤ 1) : 0 ≤ (1 - z) / (1 - (1 - x.1 * x.2) * z) ∧ (1 - z) / (1 - (1 - x.1 * x.2) * z) ≤ 1 := by constructor · apply div_nonneg (by linarith) simp only [sub_nonneg] - apply mul_le_one₀ _ (by linarith) (by linarith) + refine (mul_le_of_le_one_left (by linarith) ?_).trans (by linarith) simp only [tsub_le_iff_right, le_add_iff_nonneg_right] nlinarith · rw [div_le_iff₀] @@ -670,18 +591,20 @@ lemma ineq_aux (x : ℝ × ℝ) (z : ℝ) (hx : (0 < x.1 ∧ x.1 < 1) ∧ 0 < x. suffices z * (1 - x.1 * x.2) ≤ (1 - x.1 * x.2) by nlinarith apply mul_le_of_le_one_left (by nlinarith) hz.2 -lemma ineq_aux1 (x : ℝ × ℝ) (z : ℝ) (hx : (0 < x.1 ∧ x.1 < 1) ∧ 0 < x.2 ∧ x.2 < 1) (hz : 0 ≤ z ∧ z ≤ 1) : +lemma ineq_aux1 (x : ℝ × ℝ) (z : ℝ) (hx : (0 < x.1 ∧ x.1 < 1) ∧ 0 < x.2 ∧ x.2 < 1) (hz : 0 ≤ z + ∧ z ≤ 1) : 1 - (1 - x.1 * x.2) * z ≠ 0 := by suffices (1 - x.1 * x.2) * z < 1 by linarith rw [mul_comm] suffices z * (1 - x.1 * x.2) ≤ (1 - x.1 * x.2) by nlinarith apply mul_le_of_le_one_left (by nlinarith) hz.2 -lemma fun_eq_aux (x : ℝ × ℝ) (y : ℝ) (hx : (0 < x.1 ∧ x.1 < 1) ∧ 0 < x.2 ∧ x.2 < 1) (hy : 0 ≤ y ∧ y ≤ 1) : +lemma fun_eq_aux (x : ℝ × ℝ) (y : ℝ) (hx : (0 < x.1 ∧ x.1 < 1) ∧ 0 < x.2 ∧ x.2 < 1) (hy : 0 ≤ y + ∧ y ≤ 1) : deriv (fun z => (1 - z) / (1 - (1 - x.1 * x.2) * z)) y = (fun z => - x.1 * x.2 / (1 - (1 - x.1 * x.2) * z) ^ 2) y := by - rw [deriv_div] - · rw [deriv_const_sub, deriv_const_sub, deriv_const_mul _ differentiableAt_id'] + rw [deriv_fun_div] + · rw [deriv_const_sub, deriv_const_sub, deriv_const_mul _ differentiableAt_id] simp only [deriv_id'', neg_mul, one_mul, neg_sub, mul_one] congr ring @@ -689,9 +612,12 @@ lemma fun_eq_aux (x : ℝ × ℝ) (y : ℝ) (hx : (0 < x.1 ∧ x.1 < 1) ∧ 0 < · apply DifferentiableAt.const_sub (DifferentiableAt.const_mul differentiableAt_id _) · exact ineq_aux1 x y hx hy -lemma double_integral_eq2 (n : ℕ) (x : ℝ × ℝ) (hx : x ∈ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1) : ∫ (z : ℝ) in Set.Ioo 0 1, - eval x.1 (shiftedLegendre n) * (x.1 * x.2 * z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z) ^ (n + 1) = - ∫ (z : ℝ) in Set.Ioo 0 1, eval x.1 (shiftedLegendre n) * (1 - z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z) := by +lemma double_integral_eq2 (n : ℕ) (x : ℝ × ℝ) (hx : x ∈ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1) : ∫ (z : ℝ) + in Set.Ioo 0 1, + eval x.1 (aperyShiftedLegendre n) * (x.1 * x.2 * z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * + x.2) * z) ^ (n + 1) = + ∫ (z : ℝ) in Set.Ioo 0 1, eval x.1 (aperyShiftedLegendre n) * (1 - z) ^ n * (1 - x.2) ^ n / + (1 - (1 - x.1 * x.2) * z) := by rw [← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by norm_num), ← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by norm_num)] simp only [← mul_div, mul_assoc] @@ -712,7 +638,7 @@ lemma double_integral_eq2 (n : ℕ) (x : ℝ × ℝ) (hx : x ∈ Set.Ioo 0 1 × apply ContinuousOn.mul continuousOn_const continuousOn_id · intro y hy simp only [Set.mem_prod, Set.mem_Ioo, zero_le_one, Set.uIcc_of_le, Set.mem_Icc, - OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff] at hx hy ⊢ + ] at hx hy ⊢ apply pow_ne_zero exact ineq_aux1 x y hx hy · intro y hy @@ -754,7 +680,8 @@ lemma double_integral_eq2 (n : ℕ) (x : ℝ × ℝ) (hx : x ∈ Set.Ioo 0 1 × 1 - (1 - y) / (1 - (1 - x.1 * x.2) * y) := by rw [sub_div, div_self (ineq_aux1 x y hx hy)] have eq2 : ((1 - (1 - x.1 * x.2) * y) - (1 - x.1 * x.2) * (1 - y)) / - (1 - (1 - x.1 * x.2) * y) = 1 - (1 - x.1 * x.2) * ((1 - y) / (1 - (1 - x.1 * x.2) * y)) := by + (1 - (1 - x.1 * x.2) * y) = 1 - (1 - x.1 * x.2) * ((1 - y) / (1 - (1 - x.1 * x.2) + * y)) := by rw [sub_div, div_self (ineq_aux1 x y hx hy), mul_div] rw [div_eq_iff] · rw [← eq1, ← eq2, mul_div, div_eq_div_iff (ineq_aux1 x y hx hy) (ineq_aux1 x y hx hy)] @@ -774,14 +701,15 @@ lemma double_integral_eq2 (n : ℕ) (x : ℝ × ℝ) (hx : x ∈ Set.Ioo 0 1 × · intro y hy simp only [Set.mem_Icc] at hy exact ineq_aux1 x y hx hy - _ = ∫ (y : ℝ) in (0)..1, x.1 * x.2 / (1 - (1 - x.1 * x.2) * y) ^ 2 * (1 - g y) ^ n / (1 - (1 - x.1 * x.2) * g y) := by + _ = ∫ (y : ℝ) in (0)..1, x.1 * x.2 / (1 - (1 - x.1 * x.2) * y) ^ 2 * (1 - g y) ^ n / (1 - (1 + - x.1 * x.2) * g y) := by rw [← intervalIntegral.integral_neg] apply intervalIntegral.integral_congr intro y hy simp only [zero_le_one, Set.uIcc_of_le, Set.mem_Icc] at hy ⊢ - simp only [g, g'] + simp only [g] rw [fun_eq_aux x y hx hy] - simp [g, g', neg_div] + ring _ = ∫ (y : ℝ) in (0)..1, (x.1 * x.2 * y) ^ n / (1 - (1 - x.1 * x.2) * y) ^ (n + 1) := by apply intervalIntegral.integral_congr intro y hy @@ -795,7 +723,7 @@ lemma double_integral_eq2 (n : ℕ) (x : ℝ × ℝ) (hx : x ∈ Set.Ioo 0 1 × rw [div_mul_eq_mul_div, div_div, div_eq_div_iff] · simp only [← eq1, sub_sub_sub_cancel_left, div_pow, ← eq2, g] rw [mul_div, mul_comm, mul_div, mul_div, mul_div, div_eq_div_iff] - ring + · ring · apply pow_ne_zero exact ineq_aux1 x y hx hy · exact ineq_aux1 x y hx hy @@ -812,39 +740,43 @@ lemma double_integral_eq2 (n : ℕ) (x : ℝ × ℝ) (hx : x ∈ Set.Ioo 0 1 × exact ineq_aux1 x y hx hy lemma eq3_integrableOn_aux (n : ℕ) (z : ℝ) (hz : z ∈ Set.Ioo 0 1) : - MeasureTheory.Integrable (fun x ↦ eval x.1 (shiftedLegendre n) * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z)) - ((MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo 0 1))) := by + MeasureTheory.Integrable (fun x ↦ eval x.1 (aperyShiftedLegendre n) * (1 - x.2) ^ n / (1 - + (1 - x.1 * x.2) * z)) + ((MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo + 0 1))) := by rw [MeasureTheory.Measure.prod_restrict, ← MeasureTheory.Measure.volume_eq_prod] apply MeasureTheory.IntegrableOn.integrable apply MeasureTheory.IntegrableOn.mono_set (t := Set.Icc 0 1 ×ˢ Set.Icc 0 1) - apply ContinuousOn.integrableOn_compact - · simp only [Set.mem_Ioo, Set.Icc_prod_Icc, Prod.mk_zero_zero, Prod.mk_one_one,isCompact_Icc] - · simp only [shiftedLegendre_eq_sum, map_pow, map_neg, map_one, smul_eq_mul] - apply ContinuousOn.div - · apply ContinuousOn.mul - simp only [eval_finset_sum, eval_mul, eval_pow, eval_neg, eval_one, eval_natCast, eval_X] - apply continuousOn_finset_sum - intro i _ - apply ContinuousOn.mul continuousOn_const - apply ContinuousOn.pow continuousOn_fst - apply ContinuousOn.pow (ContinuousOn.sub continuousOn_const continuousOn_snd) - · apply ContinuousOn.sub continuousOn_const - apply ContinuousOn.mul _ continuousOn_const - apply ContinuousOn.sub continuousOn_const - apply ContinuousOn.mul continuousOn_fst continuousOn_snd - · intro x hx - suffices 1 - (1 - x.1 * x.2) * z > 0 by linarith - simp only [Set.mem_prod, Set.mem_Icc] at hx - simp only [Set.mem_Ioo, gt_iff_lt, sub_pos] at hz ⊢ - suffices (1 - x.1 * x.2) * z ≤ z by linarith - apply mul_le_of_le_one_left (by linarith) - simp only [tsub_le_iff_right, le_add_iff_nonneg_right] - nlinarith + · apply ContinuousOn.integrableOn_compact + · simp only [Set.Icc_prod_Icc, Prod.mk_zero_zero, Prod.mk_one_one,isCompact_Icc] + · simp only [shiftedLegendre_eq_sum, map_pow, map_neg, map_one] + apply ContinuousOn.div + · apply ContinuousOn.mul + · simp only [eval_finsetSum, eval_mul, eval_pow, eval_neg, eval_one, eval_natCast, eval_X] + apply continuousOn_finsetSum + intro i _ + apply ContinuousOn.mul continuousOn_const + apply ContinuousOn.pow continuousOn_fst + · apply ContinuousOn.pow (ContinuousOn.sub continuousOn_const continuousOn_snd) + · apply ContinuousOn.sub continuousOn_const + apply ContinuousOn.mul _ continuousOn_const + apply ContinuousOn.sub continuousOn_const + apply ContinuousOn.mul continuousOn_fst continuousOn_snd + · intro x hx + suffices 1 - (1 - x.1 * x.2) * z > 0 by linarith + simp only [Set.mem_prod, Set.mem_Icc] at hx + simp only [Set.mem_Ioo, gt_iff_lt, sub_pos] at hz ⊢ + suffices (1 - x.1 * x.2) * z ≤ z by linarith + apply mul_le_of_le_one_left (by linarith) + simp only [tsub_le_iff_right, le_add_iff_nonneg_right] + nlinarith · apply Set.prod_mono Set.Ioo_subset_Icc_self Set.Ioo_subset_Icc_self -lemma double_integral_eq3 (n : ℕ) (z : ℝ) (hz : z ∈ Set.Ioo 0 1) : ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, +lemma double_integral_eq3 (n : ℕ) (z : ℝ) (hz : z ∈ Set.Ioo 0 1) : ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 + ×ˢ Set.Ioo 0 1, (x.1 * x.2 * z * (1 - x.1) * (1 - x.2)) ^ n / (1 - (1 - x.1 * x.2) * z) ^ (n + 1) = - ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, eval x.1 (shiftedLegendre n) * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z) := by + ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, eval x.1 (aperyShiftedLegendre n) * (1 - x.2) + ^ n / (1 - (1 - x.1 * x.2) * z) := by symm rw [MeasureTheory.Measure.volume_eq_prod, ← MeasureTheory.Measure.prod_restrict, MeasureTheory.integral_prod, MeasureTheory.integral_integral_swap] @@ -852,25 +784,30 @@ lemma double_integral_eq3 (n : ℕ) (z : ℝ) (hz : z ∈ Set.Ioo 0 1) : ∫ (x simp only calc _ = ∫ (y : ℝ) in Set.Ioo 0 1, (1 - y) ^ n * ∫ (x : ℝ) in Set.Ioo 0 1, - eval x (shiftedLegendre n) / (1 - (1 - x * y) * z) := by + eval x (aperyShiftedLegendre n) / (1 - (1 - x * y) * z) := by apply MeasureTheory.setIntegral_congr_fun (by measurability) intro y hy - simp at hy ⊢ - rw [← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by norm_num), - ← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by norm_num), + simp only at hy ⊢ + rw [← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by + norm_num), + ← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by + norm_num), ← intervalIntegral.integral_const_mul] simp [mul_div, mul_comm] - _ = ∫ (y : ℝ) in Set.Ioo 0 1, (1 - y) ^ n * ∫ (x : ℝ) in (0)..1, (y * x * z) ^ n * (1 - x) ^ n / (1 - (1 - y * x) * z) ^ (n + 1) := by + _ = ∫ (y : ℝ) in Set.Ioo 0 1, (1 - y) ^ n * ∫ (x : ℝ) in (0)..1, (y * x * z) ^ n * (1 - x) + ^ n / (1 - (1 - y * x) * z) ^ (n + 1) := by apply MeasureTheory.setIntegral_congr_fun (by measurability) intro y hy simp only congr 1 - rw [← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by norm_num)] + rw [← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by + norm_num)] have := legendre_integral_special n hy hz simp only [mul_one_div] at this simp only [← this] simp only [mul_comm] - _ = ∫ (y : ℝ) in Set.Ioo 0 1, ∫ (x : ℝ) in Set.Ioo 0 1, (1 - y) ^ n * (y * x * z) ^ n * (1 - x) ^ n / (1 - (1 - y * x) * z) ^ (n + 1) := by + _ = ∫ (y : ℝ) in Set.Ioo 0 1, ∫ (x : ℝ) in Set.Ioo 0 1, (1 - y) ^ n * (y * x * z) ^ n * (1 + - x) ^ n / (1 - (1 - y * x) * z) ^ (n + 1) := by apply MeasureTheory.setIntegral_congr_fun (by measurability) intro y _ simp only @@ -885,26 +822,26 @@ lemma double_integral_eq3 (n : ℕ) (z : ℝ) (hz : z ∈ Set.Ioo 0 1) : ∫ (x · rw [MeasureTheory.Measure.prod_restrict, ← MeasureTheory.Measure.volume_eq_prod] apply MeasureTheory.IntegrableOn.integrable apply MeasureTheory.IntegrableOn.mono_set (t := Set.Icc 0 1 ×ˢ Set.Icc 0 1) - apply ContinuousOn.integrableOn_compact - · simp only [Set.Icc_prod_Icc, Prod.mk_zero_zero, Prod.mk_one_one, isCompact_Icc] - · apply ContinuousOn.div - · apply ContinuousOn.pow - apply ContinuousOn.mul _ (ContinuousOn.sub continuousOn_const continuousOn_snd) - apply ContinuousOn.mul _ (ContinuousOn.sub continuousOn_const continuousOn_fst) - apply ContinuousOn.mul _ continuousOn_const - apply ContinuousOn.mul continuousOn_fst continuousOn_snd - · apply ContinuousOn.pow - apply ContinuousOn.sub continuousOn_const _ - apply ContinuousOn.mul _ continuousOn_const - apply ContinuousOn.sub continuousOn_const _ - apply ContinuousOn.mul continuousOn_fst continuousOn_snd - · intro x hx - simp only [Set.mem_prod, Set.mem_Icc, Set.mem_Ioo] at hx hz - apply pow_ne_zero - suffices (1 - x.1 * x.2) * z ≤ z by linarith - apply mul_le_of_le_one_left (by linarith) - simp only [tsub_le_iff_right, le_add_iff_nonneg_right] - nlinarith + · apply ContinuousOn.integrableOn_compact + · simp only [Set.Icc_prod_Icc, Prod.mk_zero_zero, Prod.mk_one_one, isCompact_Icc] + · apply ContinuousOn.div + · apply ContinuousOn.pow + apply ContinuousOn.mul _ (ContinuousOn.sub continuousOn_const continuousOn_snd) + apply ContinuousOn.mul _ (ContinuousOn.sub continuousOn_const continuousOn_fst) + apply ContinuousOn.mul _ continuousOn_const + apply ContinuousOn.mul continuousOn_fst continuousOn_snd + · apply ContinuousOn.pow + apply ContinuousOn.sub continuousOn_const _ + apply ContinuousOn.mul _ continuousOn_const + apply ContinuousOn.sub continuousOn_const _ + apply ContinuousOn.mul continuousOn_fst continuousOn_snd + · intro x hx + simp only [Set.mem_prod, Set.mem_Icc, Set.mem_Ioo] at hx hz + apply pow_ne_zero + suffices (1 - x.1 * x.2) * z ≤ z by linarith + apply mul_le_of_le_one_left (by linarith) + simp only [tsub_le_iff_right, le_add_iff_nonneg_right] + nlinarith · apply Set.prod_mono Set.Ioo_subset_Icc_self Set.Ioo_subset_Icc_self · exact eq3_integrableOn_aux n z hz · exact eq3_integrableOn_aux n z hz @@ -913,35 +850,42 @@ theorem JJ_eq_form (n : ℕ) : JJ n = JJ' n := by simp only [JJ, JJ'] calc _ = ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, - (∫ (z : ℝ) in Set.Ioo 0 1, eval x.1 (shiftedLegendre n) * eval x.2 (shiftedLegendre n) * (1 / (1 - (1 - x.1 * x.2) * z))) := by + (∫ (z : ℝ) in Set.Ioo 0 1, eval x.1 (aperyShiftedLegendre n) * eval x.2 + (aperyShiftedLegendre n) * (1 / (1 - (1 - x.1 * x.2) * z))) := by apply MeasureTheory.setIntegral_congr_fun (by measurability) intro x hx simp only [Set.mem_prod, Set.mem_Ioo] at hx ⊢ rw [mul_assoc, mul_comm, ← integral1, ← MeasureTheory.integral_Ioc_eq_integral_Ioo, - ← intervalIntegral.integral_of_le (by norm_num), intervalIntegral.integral_const_mul] <;> nlinarith + ← intervalIntegral.integral_of_le (by norm_num), intervalIntegral.integral_const_mul] <;> + nlinarith _ = ∫ (z : ℝ) in Set.Ioo 0 1, ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, - eval x.1 (shiftedLegendre n) * eval x.2 (shiftedLegendre n) * (1 / (1 - (1 - x.1 * x.2) * z)) := by + eval x.1 (aperyShiftedLegendre n) * eval x.2 (aperyShiftedLegendre n) * (1 / (1 - (1 - x.1 + * x.2) * z)) := by symm rw [MeasureTheory.integral_integral_swap] exact integrableOn_JJ1 n _ = ∫ (z : ℝ) in Set.Ioo 0 1, ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, - eval x.1 (shiftedLegendre n) * (x.1 * x.2 * z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z) ^ (n + 1) := by + eval x.1 (aperyShiftedLegendre n) * (x.1 * x.2 * z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * + x.2) * z) ^ (n + 1) := by apply MeasureTheory.setIntegral_congr_fun (by measurability) intro z hz simp only exact double_integral_eq1 n z hz _ = ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, ∫ (z : ℝ) in Set.Ioo 0 1, - eval x.1 (shiftedLegendre n) * (x.1 * x.2 * z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z) ^ (n + 1) := by + eval x.1 (aperyShiftedLegendre n) * (x.1 * x.2 * z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * + x.2) * z) ^ (n + 1) := by rw [MeasureTheory.integral_integral_swap] exact integrableOn_JJ2 n _ = ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, ∫ (z : ℝ) in Set.Ioo 0 1, - eval x.1 (shiftedLegendre n) * (1 - z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z) := by + eval x.1 (aperyShiftedLegendre n) * (1 - z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z) + := by apply MeasureTheory.setIntegral_congr_fun (by measurability) intro x hx simp only exact double_integral_eq2 n x hx _ = ∫ (z : ℝ) in Set.Ioo 0 1, ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, - eval x.1 (shiftedLegendre n) * (1 - z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z) := by + eval x.1 (aperyShiftedLegendre n) * (1 - z) ^ n * (1 - x.2) ^ n / (1 - (1 - x.1 * x.2) * z) + := by symm rw [MeasureTheory.integral_integral_swap] exact integrableOn_JJ3 n @@ -957,7 +901,8 @@ theorem JJ_eq_form (n : ℕ) : JJ n = JJ' n := by rw [smul_eq_mul] ring _ = ∫ (z : ℝ) in Set.Ioo 0 1, ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, - (x.1 * x.2 * z * (1 - x.1) * (1 - x.2) * (1 - z)) ^ n / (1 - (1 - x.1 * x.2) * z) ^ (n + 1) := by + (x.1 * x.2 * z * (1 - x.1) * (1 - x.2) * (1 - z)) ^ n / (1 - (1 - x.1 * x.2) * z) ^ (n + 1) + := by apply MeasureTheory.setIntegral_congr_fun (by measurability) intro z hz simp only @@ -968,7 +913,8 @@ theorem JJ_eq_form (n : ℕ) : JJ n = JJ' n := by rw [smul_eq_mul, mul_comm, mul_div, ← mul_pow] ring _ = ∫ (x : ℝ × ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, - (x.2.1 * (1 - x.2.1) * x.2.2 * (1 - x.2.2) * x.1 * (1 - x.1) / (1 - (1 - x.2.1 * x.2.2) * x.1)) ^ n / + (x.2.1 * (1 - x.2.1) * x.2.2 * (1 - x.2.2) * x.1 * (1 - x.1) / (1 - (1 - x.2.1 * x.2.2) * + x.1)) ^ n / (1 - (1 - x.2.1 * x.2.2) * x.1) := by symm rw [MeasureTheory.Measure.volume_eq_prod, ← MeasureTheory.Measure.prod_restrict, @@ -992,38 +938,16 @@ theorem JJ_pos (n : ℕ) : 0 < JJ n := by have subset : Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 ⊆ Function.support F := by intro a ha change F a ≠ 0 - simp only [div_pow, ne_eq, _root_.div_eq_zero_iff, pow_eq_zero_iff', mul_eq_zero, not_or, - not_and, Decidable.not_not, F] + have hden := pos_aux a (by simpa only [Set.mem_prod, Set.mem_Ioo] using ha) simp only [Set.mem_prod, Set.mem_Ioo] at ha rcases ha with ⟨⟨hx0, hx1⟩, ⟨hy0, hy1⟩, hz0, hz1⟩ - constructor - · constructor - · intro h - rcases h with (h | h); swap; nlinarith - rcases h with (h | h); swap; nlinarith - rcases h with (h | h); swap; nlinarith - rcases h with (h | h); swap; nlinarith - rcases h with (h | h) <;> nlinarith - · intro h - suffices ¬1 - (1 - a.2.1 * a.2.2) * a.1 = 0 by tauto - suffices 1 - (1 - a.2.1 * a.2.2) * a.1 > 0 by linarith - simp only [gt_iff_lt, sub_pos] - suffices (1 - a.2.1 * a.2.2) * a.1 < a.1 by linarith - rw [mul_lt_iff_lt_one_left] - · simp only [sub_lt_self_iff] - nlinarith - · exact hx0 - · suffices 1 - (1 - a.2.1 * a.2.2) * a.1 > 0 by linarith - simp only [gt_iff_lt, sub_pos] - suffices (1 - a.2.1 * a.2.2) * a.1 < a.1 by linarith - rw [mul_lt_iff_lt_one_left] - · simp only [sub_lt_self_iff] - nlinarith - · exact hx0 + apply ne_of_gt + dsimp only [F] + positivity rw [MeasureTheory.Measure.restrict_apply'] - rw [Set.inter_eq_right.2 subset] - simp only [MeasureTheory.Measure.volume_eq_prod, MeasureTheory.Measure.prod_prod] - simp only [Real.volume_Ioo, sub_zero, ENNReal.ofReal_one, mul_one, zero_lt_one] + · rw [Set.inter_eq_right.2 subset] + simp only [MeasureTheory.Measure.volume_eq_prod, MeasureTheory.Measure.prod_prod] + simp only [Real.volume_Ioo, sub_zero, ENNReal.ofReal_one, mul_one, zero_lt_one] · measurability · apply MeasureTheory.ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter · rw [MeasureTheory.IntegrableOn] @@ -1041,10 +965,10 @@ theorem JJ_pos (n : ℕ) : 0 < JJ n := by apply mul_nonneg _ (by linarith) apply mul_nonneg _ (by linarith) apply mul_nonneg (by linarith) (by linarith) - · simp only [abs_eq_self, sub_nonneg] - apply mul_le_one₀ (by nlinarith) (by linarith) (by linarith) - · simp only [abs_eq_self, sub_nonneg] - apply mul_le_one₀ (by nlinarith) (by linarith) (by linarith) + · simp only [sub_nonneg] + exact (mul_le_of_le_one_left (by linarith) (by nlinarith)).trans (by linarith) + · simp only [sub_nonneg] + exact (mul_le_of_le_one_left (by linarith) (by nlinarith)).trans (by linarith) · rw [Set.mem_inter_iff] at hx tauto · exact integrableOn_JJ' n @@ -1078,12 +1002,13 @@ lemma Summable_of_zeta_two' : Summable (fun (n : ℕ) ↦ 1 / ((n : ℝ) + 1) ^ exact h lemma zeta_3_pos : 0 < ∑' (n : ℕ), 1 / ((n : ℝ) + 1) ^ 3 := by - apply tsum_pos (ι := ℕ) (g := fun n => 1 / ((n : ℝ) + 1) ^ 3) (i := 1) + apply Summable.tsum_pos (ι := ℕ) (g := fun n => 1 / ((n : ℝ) + 1) ^ 3) (i := 1) · apply summable_of_sum_range_le (c := Real.pi ^ 2 / 6) · intro _ positivity · intro n - suffices ∑ i ∈ Finset.range n, 1 / ((i : ℝ) + 1) ^ 3 ≤ ∑ i ∈ Finset.range n, 1 / ((i : ℝ) + 1) ^ 2 by + suffices ∑ i ∈ Finset.range n, 1 / ((i : ℝ) + 1) ^ 3 ≤ + ∑ i ∈ Finset.range n, 1 / ((i : ℝ) + 1) ^ 2 by have : ∑ i ∈ Finset.range n, 1 / ((i : ℝ) + 1) ^ 2 ≤ Real.pi ^ 2 / 6 := by suffices ∑ i ∈ Finset.range n, 1 / ((i : ℝ) + 1) ^ 2 ≤ ∑' n : ℕ , 1 / ((n : ℝ) + 1) ^ 2 by have h : ∑' n : ℕ , 1 / ((n : ℝ) + 1) ^ 2 = (riemannZeta 2).re := by @@ -1092,10 +1017,10 @@ lemma zeta_3_pos : 0 < ∑' (n : ℕ), 1 / ((n : ℝ) + 1) ^ 3 := by norm_cast rw [h, riemannZeta_two] at this norm_cast at * - apply sum_le_tsum (s := Finset.range n) - intro i _ - positivity - exact Summable_of_zeta_two' + apply Summable.sum_le_tsum (s := Finset.range n) + · intro i _ + positivity + · exact Summable_of_zeta_two' linarith apply Finset.sum_le_sum intro i _ @@ -1104,7 +1029,7 @@ lemma zeta_3_pos : 0 < ∑' (n : ℕ), 1 / ((n : ℝ) + 1) ^ 3 := by · positivity · positivity · intro m - simp only [one_div, pow_succ, add_comm, add_left_comm] + simp only [one_div, pow_succ] positivity · positivity @@ -1133,45 +1058,18 @@ theorem JJ_upper (n : ℕ) : JJ n ≤ 2 * (1 / 24) ^ n * ∑' n : ℕ , 1 / ((n apply mul_nonneg _ (by linarith) apply mul_nonneg _ (by linarith) apply mul_nonneg (by linarith) (by linarith) - · simp only [abs_eq_self, sub_nonneg] - apply mul_le_one₀ (by nlinarith) (by linarith) (by linarith) - · simp only [abs_eq_self, sub_nonneg] - apply mul_le_one₀ (by nlinarith) (by linarith) (by linarith) + · simp only [sub_nonneg] + exact (mul_le_of_le_one_left (by linarith) (by nlinarith)).trans (by linarith) + · simp only [sub_nonneg] + exact (mul_le_of_le_one_left (by linarith) (by nlinarith)).trans (by linarith) · rw [Set.mem_inter_iff] at hx tauto - · apply AEMeasurable.aestronglyMeasurable - rw [← aemeasurable_indicator_iff (by measurability)] - apply AEMeasurable.indicator _ (by measurability) - apply AEMeasurable.div - · apply AEMeasurable.pow_const - apply AEMeasurable.div - · apply AEMeasurable.mul _ (AEMeasurable.const_sub (AEMeasurable.fst (f := id) aemeasurable_id) _) - apply AEMeasurable.mul _ (AEMeasurable.fst (f := id) aemeasurable_id) - apply AEMeasurable.mul _ (AEMeasurable.const_sub (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.2) - (AEMeasurable.snd (f := id) aemeasurable_id)) _) - apply AEMeasurable.mul _ (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.2) - (AEMeasurable.snd (f := id) aemeasurable_id)) - apply AEMeasurable.mul _ (AEMeasurable.const_sub (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.1) - (AEMeasurable.fst (f := id) aemeasurable_id)) _) - exact (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.1) - (AEMeasurable.fst (f := id) aemeasurable_id)) - · apply AEMeasurable.const_sub - apply AEMeasurable.mul _ (AEMeasurable.fst (f := id) aemeasurable_id) - apply AEMeasurable.const_sub - apply AEMeasurable.mul _ (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.2) - (AEMeasurable.snd (f := id) aemeasurable_id)) - exact (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.1) - (AEMeasurable.fst (f := id) aemeasurable_id)) - · apply AEMeasurable.const_sub - apply AEMeasurable.mul _ (AEMeasurable.fst (f := id) aemeasurable_id) - apply AEMeasurable.const_sub - apply AEMeasurable.mul _ (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.2) - (AEMeasurable.snd (f := id) aemeasurable_id)) - exact (AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.1) - (AEMeasurable.fst (f := id) aemeasurable_id)) + · apply Measurable.aestronglyMeasurable + fun_prop lemma zeta3_le_zeta2 : ∑' n : ℕ , 1 / ((n : ℝ) + 1) ^ 3 < ∑' n : ℕ , 1 / ((n : ℝ) + 1) ^ 2 := by - apply tsum_lt_tsum_of_nonneg (f := fun n => 1 / ((n : ℝ) + 1) ^ 3) (g := fun n => 1 / ((n : ℝ) + 1) ^ 2) (i := 2) + apply Summable.tsum_lt_tsum_of_nonneg (f := fun n => 1 / ((n : ℝ) + 1) ^ 3) + (g := fun n => 1 / ((n : ℝ) + 1) ^ 2) (i := 2) · intro n positivity · intro n @@ -1182,9 +1080,10 @@ lemma zeta3_le_zeta2 : ∑' n : ℕ , 1 / ((n : ℝ) + 1) ^ 3 < ∑' n : ℕ , 1 · norm_num · exact Summable_of_zeta_two' -lemma ε_N_def_of_pi_alt : ∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ n : ℕ, n ≥ N → n.primeCounting ≤ (1 + ε) * (n : ℝ) / (n : ℝ).log := by +lemma ε_N_def_of_pi_alt : ∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ n : ℕ, + n ≥ N → n.primeCounting ≤ (1 + ε) * (n : ℝ) / (n : ℝ).log := by intro ε hε - obtain ⟨c,⟨hc0, hc1⟩⟩ := pi_alt + obtain ⟨c,⟨hc0, hc1⟩⟩ := AperyPNT.pi_alt rw [Asymptotics.isLittleO_const_iff (by simp), tendsto_atTop_nhds] at hc0 specialize hc0 (Set.Ioo (-ε) ε) (by simp only [Set.mem_Ioo, Left.neg_neg_iff, hε, and_self]) (by exact isOpen_Ioo) @@ -1193,26 +1092,27 @@ lemma ε_N_def_of_pi_alt : ∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ n : ℕ, n ≥ N intro n hn have hn' : n ≥ N := by trans (⌈N⌉₊ : ℝ) - norm_cast - linarith - exact Nat.le_ceil N + · norm_cast + linarith + · exact Nat.le_ceil N specialize hN n hn' specialize hc1 n simp only [Nat.floor_natCast] at hc1 simp only [Set.mem_Ioo] at hN - rw [hc1, ← mul_div, ← mul_div, mul_le_mul_right] - linarith - apply div_pos - norm_cast - omega - apply Real.log_pos - norm_cast - omega + rw [hc1, ← mul_div, ← mul_div, mul_le_mul_iff_of_pos_right] + · linarith + · apply div_pos + · norm_cast + omega + · apply Real.log_pos + norm_cast + omega lemma eventuallyN_of_le : ∃ N : ℕ, ∀ n : ℕ, n ≥ N → ↑(d (Finset.Icc 1 n)) ^ 3 ≤ (21 : ℝ) ^ n := by have h1 : (Real.exp 1) ^ 3 < (21 : ℝ) := by suffices (2.7182818286) ^ 3 < (21 : ℝ) by - exact pow_lt_pow_left₀ Real.exp_one_lt_d9 (n := 3) (by linarith [Real.exp_pos 1]) (by simp) |>.trans this + exact pow_lt_pow_left₀ Real.exp_one_lt_d9 (n := 3) + (by linarith [Real.exp_pos 1]) (by simp) |>.trans this norm_num have h : Real.log (21 ^ (1 / 3 : ℝ)) - 1 > 0 := by simp only [gt_iff_lt, sub_pos] @@ -1232,13 +1132,14 @@ lemma eventuallyN_of_le : ∃ N : ℕ, ∀ n : ℕ, n ≥ N → ↑(d (Finset.Ic _ ≤ (n ^ (1 / 3 * Real.log 21 * ↑n / Real.log ↑n)) ^ 3 := by apply pow_le_pow_left₀ (by simp) rw [← Real.rpow_natCast, Real.rpow_le_rpow_left_iff] - exact hN - simp only [Nat.one_lt_cast] - omega + · exact hN + · simp only [Nat.one_lt_cast] + omega _ ≤ (21 : ℝ) ^ n := by rw [← Real.rpow_natCast, ← Real.rpow_mul (by simp), mul_comm] nth_rewrite 1 [← Real.exp_log (x := n) (by simp only [Nat.cast_pos]; omega)] - have h2 : Real.log ↑n * (↑3 * (1 / 3 * Real.log 21 * ↑n / Real.log ↑n)) = Real.log 21 * ↑n := by + have h2 : Real.log ↑n * (↑3 * (1 / 3 * Real.log 21 * ↑n / Real.log ↑n)) = + Real.log 21 * ↑n := by rw [← mul_assoc, mul_div, ← mul_assoc, ← mul_assoc] simp only [one_div, isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, IsUnit.mul_inv_cancel_right] @@ -1249,10 +1150,12 @@ lemma eventuallyN_of_le : ∃ N : ℕ, ∀ n : ℕ, n ≥ N → ↑(d (Finset.Ic constructor <;> omega rw [← Real.exp_one_rpow, ← Real.rpow_mul (by exact Real.exp_nonneg 1)] norm_cast - rw [h2, Real.rpow_mul (by exact Real.exp_nonneg 1), Real.exp_one_rpow, Real.exp_log (by norm_num)] + rw [h2, Real.rpow_mul (by exact Real.exp_nonneg 1), Real.exp_one_rpow, + Real.exp_log (by norm_num)] norm_cast -theorem fun1_tendsto_zero : Filter.Tendsto (fun n ↦ ENNReal.ofReal (fun1 n)) Filter.atTop (nhds 0) := by +theorem fun1_tendsto_zero : Filter.Tendsto (fun n ↦ ENNReal.ofReal (fun1 n)) Filter.atTop (nhds + 0) := by rw [ENNReal.tendsto_atTop_zero] intro ε hε if h : ε = ⊤ then simp [h] @@ -1270,13 +1173,13 @@ theorem fun1_tendsto_zero : Filter.Tendsto (fun n ↦ ENNReal.ofReal (fun1 n)) F use N.max N1 intro n hn rw [ENNReal.ofReal_le_ofReal_iff (by simp)] - suffices ↑(d (Finset.Icc 1 n)) ^ 3 * 2 * (1 / 24) ^ n * ∑' n : ℕ , 1 / ((n : ℝ) + 1) ^ 3 ≤ ε.toReal by + suffices ↑(d (Finset.Icc 1 n)) ^ 3 * 2 * (1 / 24) ^ n * ∑' n : ℕ , 1 / ((n : ℝ) + 1) ^ 3 ≤ + ε.toReal by trans ↑(d (Finset.Icc 1 n)) ^ 3 * 2 * (1 / 24) ^ n * ∑' n : ℕ , 1 / ((n : ℝ) + 1) ^ 3 - swap - exact this - rw [mul_assoc, mul_assoc] - apply mul_le_mul_of_nonneg_left _ (by simp) - linarith [JJ_upper n] + · rw [mul_assoc, mul_assoc] + apply mul_le_mul_of_nonneg_left _ (by simp) + linarith [JJ_upper n] + · exact this calc _ ≤ 2 * (21 / 24 : ℝ) ^ n * (∑' n : ℕ , 1 / ((n : ℝ) + 1) ^ 3) := by apply mul_le_mul_of_nonneg_right _ (by linarith[zeta_3_pos]) @@ -1287,7 +1190,8 @@ theorem fun1_tendsto_zero : Filter.Tendsto (fun n ↦ ENNReal.ofReal (fun1 n)) F exact hN n (le_of_max_le_left hn) _ ≤ ε.toReal := by specialize hN1 n (le_of_max_le_right hn) - rw [← ENNReal.ofReal_toReal_eq_iff.2 h, ← ENNReal.ofReal_div_of_pos (by linarith [zeta_3_pos]), + rw [← ENNReal.ofReal_toReal_eq_iff.2 h, ← ENNReal.ofReal_div_of_pos (by linarith + [zeta_3_pos]), ← ENNReal.ofReal_pow (by norm_num), ENNReal.ofReal_le_ofReal_iff] at hN1 · rw [le_div_iff₀ (by linarith [zeta_3_pos])] at hN1 linarith @@ -1301,7 +1205,7 @@ theorem zeta_3_irratoinal : ¬ ∃ r : ℚ , r = riemannZeta 3 := by norm_cast simp_rw [Nat.cast_pow, Nat.cast_add, Nat.cast_one] by_contra! r - cases' r with r hr + obtain ⟨r, hr⟩ := r let q := r.den let hq := Rat.den_nz r have prop1 := ENNReal.Tendsto.mul_const (b := (q : ENNReal)) (fun1_tendsto_zero) (by simp) @@ -1324,21 +1228,18 @@ theorem zeta_3_irratoinal : ¬ ∃ r : ℚ , r = riemannZeta 3 := by norm_cast at this ⊢ rw [ENNReal.tendsto_atTop_zero] at prop1 specialize prop1 (1/2) (by simp) - simp only [one_div, Ico_mem_nhds_iff, Set.mem_Ioo, inv_pos, Nat.ofNat_pos, and_true, Set.mem_Ico, - Filter.eventually_top] at prop1 + simp only [one_div] at prop1 rw [← one_div] at prop1 - simp only [Filter.eventually_atTop, ge_iff_le] at prop1 - cases' prop1 with a ha + simp only [ge_iff_le] at prop1 + obtain ⟨a, ha⟩ := prop1 specialize prop2 (a + 1) specialize ha (a + 1) (by simp) rw [gt_iff_lt, ← ENNReal.ofReal_lt_ofReal_iff, ENNReal.ofReal_mul' (by simp)] at prop2 - · suffices ENNReal.ofReal (fun1 (a + 1)) * ↑q < ENNReal.ofReal (fun1 (a + 1)) * ↑q by - simp only [mul_neg, eval_mul, one_div, eval_C, Function.iterate_succ, Function.comp_apply, - derivative_mul, derivative_X_pow, Nat.cast_add, Nat.cast_one, map_add, map_natCast, map_one, - add_tsub_cancel_right, iterate_map_add, eval_add, lt_self_iff_false] at this - rw [show ENNReal.ofReal ↑q = (q : ENNReal) by simp only [ENNReal.ofReal_natCast], - show ENNReal.ofReal (1 / 2) = 1 / 2 by rw [ENNReal.ofReal_div_of_pos (by norm_num)]; simp] at prop2 - apply LE.le.trans_lt (b := (1 / 2 : ENNReal)) ha prop2 + · have hhalf : ENNReal.ofReal (1 / 2 : ℝ) = (1 / 2 : ENNReal) := by + rw [ENNReal.ofReal_div_of_pos (by norm_num)] + simp + rw [ENNReal.ofReal_natCast, hhalf] at prop2 + exact not_lt_of_ge ha prop2 · apply mul_pos _ (by simp; omega) apply mul_pos _ (JJ_pos (a + 1)) apply pow_pos diff --git a/Zeta3Irrational/Bound.lean b/Zeta3Irrational/Bound.lean index 56b2726..bb10351 100644 --- a/Zeta3Irrational/Bound.lean +++ b/Zeta3Irrational/Bound.lean @@ -1,12 +1,15 @@ import Mathlib.Analysis.RCLike.Basic -import Mathlib.Data.Real.StarOrdered +import Mathlib.Analysis.Real.Sqrt + +/-! Elementary bounds for the Apéry integral, ported from the Apache-2.0 proof by +Junqi Liu and Jujian Zhang. -/ open scoped Nat open BigOperators lemma max_value {x : ℝ} (x0 : 0 < x) (x1 : x < 1) : √x * √(1 - x) ≤ ((1 / 2) : ℝ) := by rw [← Real.sqrt_mul, le_div_iff₀, ← show √4 = 2 by rw [Real.sqrt_eq_iff_eq_sq] <;> linarith, - ← Real.sqrt_mul, Real.sqrt_le_one, show x * (1 - x) * 4= 1 - (2 * x - 1)^2 by ring] <;> + ← Real.sqrt_mul, Real.sqrt_le_one, show x * (1 - x) * 4 = 1 - (2 * x - 1) ^ 2 by ring] <;> nlinarith [mul_self_nonneg (2 * x - 1)] lemma max_value' {x : ℝ} (x0 : 0 < x) (x1 : x < 1) : √x * (1 - x) ≤ ((2 / 5) : ℝ) := by @@ -22,7 +25,7 @@ lemma max_value' {x : ℝ} (x0 : 0 < x) (x1 : x < 1) : √x * (1 - x) ≤ ((2 / _ ≤ ((2 / 5) : ℝ) := by rw [Real.sqrt_le_left] <;> norm_num -lemma nonneg {x : ℝ} (_ : 0 < x) (_ : x < 1) : (0 : ℝ) ≤ √x * √(1 -x) := +lemma nonneg {x : ℝ} (_ : 0 < x) (_ : x < 1) : (0 : ℝ) ≤ √x * √(1 - x) := mul_nonneg (Real.sqrt_nonneg _) (Real.sqrt_nonneg _) lemma bound_aux (x z : ℝ) (x0 : 0 < x) (x1 : x < 1) (z0 : 0 < z) (_ : z < 1) : @@ -36,8 +39,9 @@ lemma bound_aux (x z : ℝ) (x0 : 0 < x) (x1 : x < 1) (z0 : 0 < z) (_ : z < 1) : _ = √(1 - x) * √(1 - x) + √(x * z) * √(x * z) := by ring _ = 1 - x + x * z := by rw [Real.mul_self_sqrt, Real.mul_self_sqrt] <;> linarith -lemma bound (x y z : ℝ) (x0 : 0 < x) (x1 : x < 1) (y0 : 0 < y) (y1 : y < 1) (z0 : 0 < z) (z1 : z < 1) : - x * (1 -x) * y * (1 - y) * z * (1 - z) / ((1 - (1 - z) * x) * (1 - y * z)) < (1 / 30 : ℝ) := by +lemma bound (x y z : ℝ) (x0 : 0 < x) (x1 : x < 1) (y0 : 0 < y) (y1 : y < 1) + (z0 : 0 < z) (z1 : z < 1) : + x * (1 - x) * y * (1 - y) * z * (1 - z) / ((1 - (1 - z) * x) * (1 - y * z)) < (1 / 30 : ℝ) := by have := mul_pos x0 z0 have h1 : 2 * √(1 - x) * √(x * z) ≤ 1 - (1 - z) * x := by apply bound_aux <;> assumption have h2 : 2 * √(1 - y) * √((1 - z) * y) ≤ 1 - y * z := by @@ -52,22 +56,24 @@ lemma bound (x y z : ℝ) (x0 : 0 < x) (x1 : x < 1) (y0 : 0 < y) (y1 : y < 1) (z have : 0 ≤ x.sqrt * (1 - x).sqrt := nonneg (by assumption) (by linarith) have : 0 ≤ y.sqrt * (1 - y).sqrt := nonneg (by assumption) (by linarith) calc - _ ≤ x * (1 -x) * y * (1 - y) * z * (1 - z) / (2 * √(1 - x) * √(x * z) * (1 - y * z)) := by + _ ≤ x * (1 - x) * y * (1 - y) * z * (1 - z) / (2 * √(1 - x) * √(x * z) * (1 - y * z)) := by refine div_le_div₀ (by positivity) (le_refl _) (by positivity) ?_ rwa [mul_le_mul_iff_of_pos_right] linarith - _ ≤ x * (1 -x) * y * (1 - y) * z * (1 - z) / (2 * √(1 - x) * √(x * z) * 2 * √(1 - y) * √((1 - z) * y)) := by + _ ≤ x * (1 - x) * y * (1 - y) * z * (1 - z) / + (2 * √(1 - x) * √(x * z) * 2 * √(1 - y) * √((1 - z) * y)) := by refine div_le_div₀ (by positivity) (le_refl _) (by positivity) ?_ rw [mul_assoc, mul_assoc] rw [mul_assoc] at h2 exact mul_le_mul_of_nonneg_left h2 (le_of_lt <| by positivity) - _ = √x * √(1 -x) * (√y * √(1 - y)) * (√z * √(1 - z)) / 4 := by - rw [Real.sqrt_mul, Real.sqrt_mul] - calc _ - _ = ((x * (1 - x)) * (y * (1 - y)) * (z * (1 - z))) / (4 * (√x * √(1 - x)) * (√y * √(1 - y)) * (√z * √(1 - z))) := by ring - _ = (x / √x) * ((1 - x) / √(1 - x)) * (y / √y) * ((1 - y) / √(1 -y)) * (z / √z) * ((1 - z) / √(1 - z)) / 4 := by ring + _ = √x * √(1 - x) * (√y * √(1 - y)) * (√z * √(1 - z)) / 4 := by + rw [Real.sqrt_mul (by positivity), Real.sqrt_mul (by positivity)] + calc + _ = ((x * (1 - x)) * (y * (1 - y)) * (z * (1 - z))) / + (4 * (√x * √(1 - x)) * (√y * √(1 - y)) * (√z * √(1 - z))) := by ring + _ = (x / √x) * ((1 - x) / √(1 - x)) * (y / √y) * + ((1 - y) / √(1 - y)) * (z / √z) * ((1 - z) / √(1 - z)) / 4 := by ring _ = _ := by simpa only [Real.div_sqrt] using (by ring) - all_goals linarith _ ≤ (1 / 2) * (1 / 2) * (1 / 2) / 4 := by refine div_le_div₀ (by norm_num) (mul_le_mul_of_nonneg (mul_le_mul_of_nonneg (max_value ?_ ?_) (max_value ?_ ?_) ?_ ?_) @@ -75,7 +81,8 @@ lemma bound (x y z : ℝ) (x0 : 0 < x) (x1 : x < 1) (y0 : 0 < y) (y1 : y < 1) (z linarith _ < (1 / 30 : ℝ) := by norm_num -lemma bound_aux' (x y z : ℝ) (x0 : 0 < x) (_ : x < 1) (y0 : 0 < y) (_ : y < 1) (z0 : 0 < z) (z1 : z < 1) : +lemma bound_aux' (x y z : ℝ) (x0 : 0 < x) (_ : x < 1) (y0 : 0 < y) (_ : y < 1) + (z0 : 0 < z) (z1 : z < 1) : 2 * √(1 - z) * √(x * y * z) ≤ 1 - (1 - x * y) * z := by rw [← sub_pos] at z1 have := mul_pos x0 (mul_pos y0 z0) @@ -86,7 +93,8 @@ lemma bound_aux' (x y z : ℝ) (x0 : 0 < x) (_ : x < 1) (y0 : 0 < y) (_ : y < 1) _ = √(1 - z) * √(1 - z) + √(x * y * z) * √(x * y * z) := by ring _ = 1 - z + x * y * z := by rw [Real.mul_self_sqrt, Real.mul_self_sqrt] <;> linarith -lemma bound' (x y z : ℝ) (x0 : 0 < x) (x1 : x < 1) (y0 : 0 < y) (y1 : y < 1) (z0 : 0 < z) (z1 : z < 1) : +lemma bound' (x y z : ℝ) (x0 : 0 < x) (x1 : x < 1) (y0 : 0 < y) (y1 : y < 1) + (z0 : 0 < z) (z1 : z < 1) : x * (1 - x) * y * (1 - y) * z * (1 - z) / (1 - (1 - x * y) * z) < (1 / 24 : ℝ) := by have := mul_pos x0 z0 have h1 : 2 * √(1 - x) * √(x * z) ≤ 1 - (1 - z) * x := by apply bound_aux <;> assumption @@ -102,16 +110,17 @@ lemma bound' (x y z : ℝ) (x0 : 0 < x) (x1 : x < 1) (y0 : 0 < y) (y1 : y < 1) ( have : 0 ≤ x.sqrt * (1 - x) := mul_nonneg (Real.sqrt_nonneg _) (by linarith) have : 0 ≤ y.sqrt * (1 - y) := mul_nonneg (Real.sqrt_nonneg _) (by linarith) calc - _ ≤ x * (1 -x) * y * (1 - y) * z * (1 - z) / (2 * √(1 - z) * √(x * y * z)) := by + _ ≤ x * (1 - x) * y * (1 - y) * z * (1 - z) / (2 * √(1 - z) * √(x * y * z)) := by refine div_le_div₀ (by positivity) (le_refl _) (by positivity) ?_ apply bound_aux' <;> linarith _ = √x * (1 - x) * (√y * (1 - y)) * (√z * √(1 - z)) / 2 := by - rw [Real.sqrt_mul, Real.sqrt_mul] - calc _ - _ = ((x * (1 - x)) * (y * (1 - y)) * (z * (1 - z))) / (2 * √x * √y * (√z * √(1 - z))) := by ring - _ = (x / √x) * (1 - x) * (y / √y) * (1 - y) * (z / √z) * ((1 - z) / √(1 - z)) / 2 := by ring + rw [Real.sqrt_mul (by positivity), Real.sqrt_mul (by positivity)] + calc + _ = ((x * (1 - x)) * (y * (1 - y)) * (z * (1 - z))) / + (2 * √x * √y * (√z * √(1 - z))) := by ring + _ = (x / √x) * (1 - x) * (y / √y) * (1 - y) * (z / √z) * + ((1 - z) / √(1 - z)) / 2 := by ring _ = _ := by simpa only [Real.div_sqrt] using (by ring) - all_goals nlinarith _ ≤ (2 / 5) * (2 / 5) * (1 / 2) / 2 := by refine div_le_div₀ (by norm_num) (mul_le_mul_of_nonneg (mul_le_mul_of_nonneg (max_value' ?_ ?_) (max_value' ?_ ?_) ?_ ?_) diff --git a/Zeta3Irrational/Equality.lean b/Zeta3Irrational/Equality.lean index 4fc5c29..0beb8e6 100644 --- a/Zeta3Irrational/Equality.lean +++ b/Zeta3Irrational/Equality.lean @@ -27,10 +27,10 @@ lemma integral_equality_help (s t : ℝ) (s0 : 0 < s) (s1 : s < 1) (t0 : 0 < t) · ring_nf · have _ : 0 < (1 - (1 - s) * t) * ((1 - (1 - u) * s) * (1 - (1 - t) * u)) := by rw[mul_pos_iff_of_pos_left, mul_pos_iff_of_pos_left] <;> linarith - positivity + linarith · have _ : 0 < (1 - (1 - u) * s) * (1 - (1 - t) * u) := by rw[mul_pos_iff_of_pos_left] <;> linarith - positivity + linarith · linarith · linarith rw[← intervalIntegral.integral_congr] @@ -39,22 +39,16 @@ lemma integral_equality_help (s t : ℝ) (s0 : 0 < s) (s1 : s < 1) (t0 : 0 < t) rw[inv_eq_one_div, inv_eq_one_div, inv_eq_one_div, one_div_mul_one_div] simp at b rcases b with ⟨b1, b2⟩ - rw[← not_lt] at b1 - cases' eq_or_lt_of_not_lt b1 with b11 b12 - · rw[b11] - field_simp - rw[div_eq_one_iff_eq] - ring_nf - have _ : 0 < 1 - (1 - s) * t := by linarith - positivity - · rw[← not_lt] at b2 - cases' eq_or_lt_of_not_lt b2 with b21 b22 - · rw[← b21] - field_simp - rw[div_eq_one_iff_eq] - ring_nf - have _ : 0 < 1 - (1 - s) * t := by linarith - positivity + rcases eq_or_lt_of_le b1 with b11 | b12 + · rw[← b11] + norm_num + field_simp [ne_of_gt s1, ne_of_gt (sub_pos.mpr h2)] + ring + · rcases eq_or_lt_of_le b2 with b21 | b22 + · rw[b21] + norm_num + field_simp [ne_of_gt t0, ne_of_gt (sub_pos.mpr h2)] + ring · obtain b00 := eq1 a b12 b22 rw[b00, mul_comm] @@ -99,7 +93,7 @@ lemma integral_equality (s t : ℝ) (s0 : 0 < s) (s1 : s < 1) (t0 : 0 < t) (t1 : apply IntervalIntegrable.continuousOn_mul (hg := continuousOn_const) apply intervalIntegral.intervalIntegrable_inv · intros x hx - simp only [ge_iff_le, zero_le_one, Set.uIcc_of_le, Set.mem_Icc] at hx + simp only [zero_le_one, Set.uIcc_of_le, Set.mem_Icc] at hx intro r rw [sub_eq_zero] at r have ineq3 : (1 - x) * s ≤ 1 * s := by diff --git a/Zeta3Irrational/Integral.lean b/Zeta3Irrational/Integral.lean index 15c6253..c732e9c 100644 --- a/Zeta3Irrational/Integral.lean +++ b/Zeta3Irrational/Integral.lean @@ -2,23 +2,26 @@ A formal proof of the irrationality of Riemann-Zeta(3). Author: Junqi Liu and Jujian Zhang. -/ -import Mathlib.Analysis.Normed.Field.Instances import Mathlib.Analysis.PSeries -import Mathlib.Analysis.SpecialFunctions.Integrals -import Mathlib.Data.Real.StarOrdered +import Mathlib.Analysis.SpecialFunctions.Integrals.Basic +import Mathlib.Analysis.Real.Sqrt import Mathlib.MeasureTheory.Function.AEEqOfIntegral import Mathlib.MeasureTheory.Integral.IntegralEqImproper import Mathlib.Topology.Algebra.Module.ModuleTopology -import Mathlib.Topology.Compactness.PseudometrizableLindelof +import Mathlib.Topology.Metrizable.Basic + +/-! Integral identities in the Apache-2.0 Apéry proof of Junqi Liu and Jujian Zhang. -/ open scoped Nat open BigOperators Finset +/-- The real Apéry double integral with monomial weights of degrees `r` and `s`. -/ noncomputable abbrev J (r s : ℕ) : ℝ := ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, -(x.1 * x.2).log / (1 - x.1 * x.2) * x.1 ^ r * x.2 ^ s -noncomputable abbrev J_ENN (r s : ℕ) : ENNReal := +/-- The nonnegative extended-real Apéry double integral with weights of degrees `r` and `s`. -/ +noncomputable abbrev jENN (r s : ℕ) : ENNReal := ∫⁻ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, ENNReal.ofReal (- (x.1 * x.2).log / (1 - x.1 * x.2) * x.1 ^ r * x.2 ^ s) @@ -26,7 +29,7 @@ lemma log_rpow_integral_aux (n : ℝ) (a : ℝ) (ha : 0 < a ∧ a ≤ 1) : ∫ (x : ℝ) in Set.Ioc a 1, |-x.log * x ^ n| = ∫ (x : ℝ) in Set.Ioc a 1, -x.log * x ^ n := by apply MeasureTheory.setIntegral_congr_fun (by measurability) intro x hx - simp only [gt_iff_lt, Set.mem_Ioc, neg_mul, abs_neg, abs_eq_neg_self] at * + simp only [Set.mem_Ioc, neg_mul, abs_neg, abs_eq_neg_self] at * rw [mul_nonpos_iff] right constructor @@ -42,7 +45,7 @@ lemma log_rpow_integral' (n : ℝ) (hn : n > -1) (a : ℝ) (ha : 0 < a ∧ a ≤ f 1 - f a by simp[f], ← intervalIntegral.integral_of_le ha.2] refine intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le ha.2 (a := a) (b := 1) (f := f) (f' := fun x : ℝ => -x.log * x ^ n ) ?_ ?_ ?_ - · simp [f] + · simp only [f] refine ContinuousOn.sub (ContinuousOn.div_const ?_ (((n : ℝ) + 1) ^ 2)) ?_ · apply ContinuousOn.rpow_const continuousOn_id intro x hx @@ -77,7 +80,8 @@ lemma log_rpow_integral' (n : ℝ) (hn : n > -1) (a : ℝ) (ha : 0 < a ∧ a ≤ norm_cast apply Real.hasDerivAt_rpow_const left ; linarith - · have h : x ^ n * x.log + x ^ n / (↑n + 1) = ((↑n + 1) * x ^ n * x.log + x ^ n) / (↑n + 1) := by + · have h : x ^ n * x.log + x ^ n / (↑n + 1) = + ((↑n + 1) * x ^ n * x.log + x ^ n) / (↑n + 1) := by rw [add_div] congr 1 rw [eq_div_iff (by linarith)] @@ -104,12 +108,14 @@ lemma log_rpow_integral' (n : ℝ) (hn : n > -1) (a : ℝ) (ha : 0 < a ∧ a ≤ simp only [Set.mem_Icc, id_eq, ne_eq] at hx ⊢ nlinarith -lemma log_rpow_integrable (n : ℝ) (hn : n > -1) : IntervalIntegrable (fun x ↦ -Real.log x * x ^ n) MeasureTheory.volume 0 1 := by +lemma log_rpow_integrable (n : ℝ) (hn : n > -1) : + IntervalIntegrable (fun x ↦ -Real.log x * x ^ n) MeasureTheory.volume 0 1 := by let f := fun (x : ℝ) => -x.log * x ^ n apply MeasureTheory.IntegrableOn.intervalIntegrable rw [Set.uIcc_of_le (by norm_num), integrableOn_Icc_iff_integrableOn_Ioc] apply MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded_left (f := f) - (l := Filter.atTop) (a := fun (n : ℕ) => 1 / (n + 1 : ℝ)) (a₀ := 0) (b := 1) (I := 1 / (n + 1) ^ 2) + (l := Filter.atTop) (a := fun (n : ℕ) => 1 / (n + 1 : ℝ)) (a₀ := 0) (b := 1) + (I := 1 / (n + 1) ^ 2) · intro i simp only [one_div, f] have hi : 0 < ((i : ℝ) + 1)⁻¹ ∧ ((i : ℝ) + 1)⁻¹ ≤ 1 := by @@ -137,7 +143,7 @@ lemma log_rpow_integrable (n : ℝ) (hn : n > -1) : IntervalIntegrable (fun x · rw [log_rpow_integral' n hn] · set k := _ change _ - k ≤ _ - simp only [Real.log_inv, tsub_le_iff_right, le_add_iff_nonneg_right, + simp only [tsub_le_iff_right, le_add_iff_nonneg_right, sub_nonneg, k] rw [div_le_div_iff₀ (by linarith) (by nlinarith), mul_assoc, mul_le_mul_iff_of_pos_left] · trans 0 @@ -164,7 +170,8 @@ lemma log_rpow_integral (n : ℝ) (hn : n > -1) : ∫ (x : ℝ) in (0)..1, -x.log * x ^ n = 1 / (n + 1) ^ 2 := by let F := fun (x : ℝ) => x ^ (n + 1) * (1 - (n + 1) * x.log) / (n + 1) ^ 2 have h1 : 1 /(n + 1) ^ 2 = F 1 - F 0 := by - simp [F] + simp only [F, Real.one_rpow, Real.log_one, mul_zero, sub_zero, + Real.log_zero, mul_one] rw [Real.zero_rpow (by linarith), zero_div, sub_zero] rw [h1] refine intervalIntegral.integral_eq_sub_of_hasDerivAt_of_tendsto (by norm_num) (a := 0) (b := 1) @@ -211,7 +218,7 @@ lemma log_rpow_integral (n : ℝ) (hn : n > -1) : exact fun ⦃U⦄ a ↦ a · right; linarith · apply Filter.Tendsto.div_const - simp [← mul_assoc, ← mul_rotate (c := n + 1)] + simp only [← mul_assoc, ← mul_rotate (c := n + 1)] nth_rw 3 [show (0 : ℝ) = 0 * (n + 1) by simp] apply Filter.Tendsto.mul_const apply tendsto_log_mul_rpow_nhdsGT_zero @@ -303,42 +310,22 @@ lemma ENN_pow_integral (n : ℕ) : ∫⁻ (x : ℝ) in Set.Ioo 0 1, · tauto · omega -lemma AEMeasurable_aux : AEMeasurable (fun (x : ℝ × ℝ × ℝ) ↦ +lemma AEMeasurable_aux {r s : ℕ} : AEMeasurable (fun (x : ℝ × ℝ × ℝ) ↦ 1 / (1 - (1 - x.2.1 * x.2.2) * x.1) * x.2.1 ^ r * x.2.2 ^ s) MeasureTheory.volume := by - apply AEMeasurable.mul - · apply AEMeasurable.mul - · apply AEMeasurable.const_div - apply AEMeasurable.const_sub - apply AEMeasurable.mul _ (AEMeasurable.fst (f := id) aemeasurable_id) - · apply AEMeasurable.const_sub - apply AEMeasurable.mul - · apply AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.1) - exact AEMeasurable.fst (f := id) aemeasurable_id - · apply AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.2) - exact AEMeasurable.snd (f := id) aemeasurable_id - · apply AEMeasurable.pow_const - apply AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.1) - exact AEMeasurable.fst (f := id) aemeasurable_id - · apply AEMeasurable.pow_const - apply AEMeasurable.snd (f := fun (x : ℝ × ℝ) => x.2) - exact AEMeasurable.snd (f := id) aemeasurable_id + fun_prop lemma integral1 {a : ℝ} (ha : 0 < a) (ha1 : a < 1) : ∫ (z : ℝ) in (0)..1, 1 / (1 - (1 - a) * z) = - a.log / (1 - a) := by rw[← sub_pos] at ha1 have eq1 := intervalIntegral.integral_comp_mul_left (a := 0) (b := 1) (c := 1 - a) (f := fun z ↦ (1 - z)⁻¹) (by positivity) - have eq2 := intervalIntegral.mul_integral_comp_sub_mul (a := 0) (b := 1 - a) (f := fun x ↦ (x)⁻¹) - (c := 1) (d := 1) have eq3 := integral_inv_of_pos (a := a) (b := 1) ha (by norm_num) simp only [mul_zero, mul_one, smul_eq_mul] at eq1 simp only [one_div] rw [eq1, inv_mul_eq_div] field_simp simp only [one_div] - simp only [one_mul, intervalIntegral.integral_comp_sub_left, sub_sub_cancel, sub_zero, - mul_zero] at eq2 - rw[eq3] + rw [intervalIntegral.integral_comp_sub_left, sub_sub_cancel, sub_zero, eq3] simp lemma sub_mul_mul_ne_zero (y : ℝ) (x : ℝ × ℝ) @@ -348,7 +335,7 @@ lemma sub_mul_mul_ne_zero (y : ℝ) (x : ℝ × ℝ) by_cases hy' : y = 0 · rw [hy'] simp - · simp only [Set.mem_prod, Set.mem_Ioo, sub_pos, Set.mem_Icc, gt_iff_lt, sub_pos] at * + · simp only [sub_pos, Set.mem_Icc] at * suffices (1 - x.1 * x.2) * y < y by linarith rwa [mul_lt_iff_lt_one_left] rcases hy with ⟨hy1, _⟩ @@ -357,7 +344,7 @@ lemma sub_mul_mul_ne_zero (y : ℝ) (x : ℝ × ℝ) linarith lemma integrableOn_aux (x : ℝ × ℝ) - (h1 : 0 < 1 - (1 - x.1 * x.2)) (h2 : 1 - (1 - x.1 * x.2) < 1): + (h1 : 0 < 1 - (1 - x.1 * x.2)) (h2 : 1 - (1 - x.1 * x.2) < 1) : MeasureTheory.IntegrableOn (fun t ↦ 1 / (1 - (1 - x.1 * x.2) * t)) (Set.Ioo 0 1) MeasureTheory.volume := by rw [← integrableOn_Ioc_iff_integrableOn_Ioo] @@ -392,8 +379,7 @@ lemma integrableOn_aux (x : ℝ × ℝ) simp at hy apply div_nonneg (by norm_num) simp only [sub_nonneg] - apply mul_le_one₀ _ (by linarith) (by linarith) - linarith + exact (mul_le_of_le_one_left (by linarith) (by linarith)).trans (by linarith) lemma JENN_eq_triple_aux' (x : ℝ × ℝ) (hx : x ∈ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1) : ∫⁻ (w : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (1 / (1 - (1 - x.1 * x.2) * w)) = @@ -423,11 +409,10 @@ lemma JENN_eq_triple_aux' (x : ℝ × ℝ) (hx : x ∈ Set.Ioo 0 1 ×ˢ Set.Ioo · simp only [h, true_and] at hs apply div_nonneg (by norm_num) simp only [sub_nonneg] - apply mul_le_one₀ _ (by linarith) (by linarith) - linarith + exact (mul_le_of_le_one_left (by linarith) (by linarith)).trans (by linarith) · tauto -lemma JENN_eq_triple_aux (x : ℝ × ℝ) (hx : x ∈ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1) : +lemma JENN_eq_triple_aux {r s : ℕ} (x : ℝ × ℝ) (hx : x ∈ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1) : ∫⁻ (w : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (1 / (1 - (1 - x.1 * x.2) * w) * x.1 ^ r * x.2 ^ s) = ENNReal.ofReal (-Real.log (x.1 * x.2) / (1 - x.1 * x.2) * x.1 ^ r * x.2 ^ s) := by calc @@ -454,11 +439,11 @@ lemma JENN_eq_triple_aux (x : ℝ × ℝ) (hx : x ∈ Set.Ioo 0 1 ×ˢ Set.Ioo 0 · simp only [Left.nonneg_neg_iff] apply Real.log_nonpos · apply mul_nonneg (by linarith) (by linarith) - · apply mul_le_one₀ (by linarith) (by linarith) (by linarith) + · exact (mul_le_of_le_one_left (by linarith) (by linarith)).trans (by linarith) · simp only [sub_nonneg] - apply mul_le_one₀ (by linarith) (by linarith) (by linarith) + exact (mul_le_of_le_one_left (by linarith) (by linarith)).trans (by linarith) -lemma JENN_eq_triple (r s : ℕ) : J_ENN r s = +lemma JENN_eq_triple (r s : ℕ) : jENN r s = ∫⁻ (x : ℝ × ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, ENNReal.ofReal (1 / (1 - (1 - x.2.1 * x.2.2) * x.1) * x.2.1 ^ r * x.2.2 ^ s) := by symm @@ -480,11 +465,12 @@ lemma JENN_eq_triple (r s : ℕ) : J_ENN r s = exact AEMeasurable_aux _ = ∫⁻ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, ENNReal.ofReal (- (x.1 * x.2).log / (1 - x.1 * x.2) * x.1 ^ r * x.2 ^ s) := by - apply MeasureTheory.setLIntegral_congr_fun (by measurability) <| Filter.Eventually.of_forall ?_ + apply MeasureTheory.setLIntegral_congr_fun (by measurability) intro x hx + dsimp only rw [JENN_eq_triple_aux _ hx] -lemma AEMeasurable_aux' : AEMeasurable +lemma AEMeasurable_aux' {k r s : ℕ} : AEMeasurable (fun x ↦ ENNReal.ofReal (-Real.log (x.1 * x.2) * x.1 ^ (k + r) * x.2 ^ (k + s))) (MeasureTheory.volume.restrict (Set.Ioo 0 1 ×ˢ Set.Ioo 0 1)) := by apply AEMeasurable.ennreal_ofReal @@ -551,10 +537,12 @@ lemma aux_lintegral3 (k r s : ℕ) : ∫⁻ (x : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (-x.log * x ^ (k + r) / (k + s + 1)) = ENNReal.ofReal (1 / ((k + r + 1) ^ 2 * (k + s + 1))) := by calc - _ = (∫⁻ (x : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (-x.log * x ^ (k + r))) * ENNReal.ofReal (1 / (k + s + 1)) := by + _ = (∫⁻ (x : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (-x.log * x ^ (k + r))) * + ENNReal.ofReal (1 / (k + s + 1)) := by rw [← MeasureTheory.lintegral_mul_const] - · apply MeasureTheory.setLIntegral_congr_fun (by measurability) <| Filter.Eventually.of_forall ?_ + · apply MeasureTheory.setLIntegral_congr_fun (by measurability) rintro y ⟨hy1, hy2⟩ + dsimp only rw [← ENNReal.ofReal_mul] · field_simp simp only [neg_mul, Left.nonneg_neg_iff] @@ -575,10 +563,12 @@ lemma aux_lintegral4 (k r s : ℕ) : ∫⁻ (x : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (x ^ (k + r) / (k + s + 1) ^ 2) = ENNReal.ofReal (1 / ((k + r + 1) * (k + s + 1) ^ 2)) := calc - _ = (∫⁻ (x : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (x ^ (k + r))) * ENNReal.ofReal (1 / (k + s + 1) ^ 2) := by + _ = (∫⁻ (x : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (x ^ (k + r))) * + ENNReal.ofReal (1 / (k + s + 1) ^ 2) := by rw [← MeasureTheory.lintegral_mul_const] - · apply MeasureTheory.setLIntegral_congr_fun (by measurability) <| Filter.Eventually.of_forall ?_ + · apply MeasureTheory.setLIntegral_congr_fun (by measurability) rintro y ⟨hy1, hy2⟩ + dsimp only rw [← ENNReal.ofReal_mul] · field_simp positivity @@ -588,7 +578,7 @@ lemma aux_lintegral4 (k r s : ℕ) : ∫⁻ (x : ℝ) in Set.Ioo 0 1, · norm_cast · positivity -lemma J_ENN_rs_eq_tsum_aux_intergal (r s k : ℕ): +lemma J_ENN_rs_eq_tsum_aux_intergal (r s k : ℕ) : ∫⁻ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, ENNReal.ofReal (- (x.1 * x.2).log * x.1 ^ (k + r) * x.2 ^ (k + s)) = ENNReal.ofReal (1 / ((k + r + 1) ^ 2 * (k + s + 1)) + 1 / ((k + r + 1) * (k + s + 1) ^ 2)) := by @@ -597,14 +587,17 @@ lemma J_ENN_rs_eq_tsum_aux_intergal (r s k : ℕ): · calc _ = ∫⁻ (x : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (- x.log * x ^ (k + r) / (k + s + 1) + x ^ (k + r) / (k + s + 1) ^ 2) := by - apply MeasureTheory.setLIntegral_congr_fun (by measurability) <| Filter.Eventually.of_forall ?_ + apply MeasureTheory.setLIntegral_congr_fun (by measurability) intro x hx + dsimp only simp only [neg_mul] - have h2 : ∫⁻ (y : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (-((x * y).log * x ^ (k + r) * y ^ (k + s))) + have h2 : ∫⁻ (y : ℝ) in Set.Ioo 0 1, + ENNReal.ofReal (-((x * y).log * x ^ (k + r) * y ^ (k + s))) = ∫⁻ (y : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (-(x.log * x ^ (k + r) * y ^ (k + s))) + ENNReal.ofReal (-(y.log * x ^ (k + r) * y ^ (k + s))) := by - apply MeasureTheory.setLIntegral_congr_fun (by measurability) <| Filter.Eventually.of_forall ?_ + apply MeasureTheory.setLIntegral_congr_fun (by measurability) intro y hy + dsimp only simp only [← neg_mul] simp only [Set.mem_Ioo] at hx hy rw [Real.log_mul (by linarith) (by linarith), neg_add, add_mul, add_mul, @@ -639,9 +632,11 @@ lemma J_ENN_rs_eq_tsum_aux_intergal (r s k : ℕ): have h2 : ∫⁻ (x : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (- x.log * x ^ (k + r) / (k + s + 1) + x ^ (k + r) / (k + s + 1) ^ 2) = ∫⁻ (x : ℝ) in Set.Ioo 0 1, - ENNReal.ofReal (-x.log * x ^ (k + r) / (k + s + 1)) + ENNReal.ofReal (x ^ (k + r) / (k + s + 1) ^ 2) := by - apply MeasureTheory.setLIntegral_congr_fun (by measurability) <| Filter.Eventually.of_forall ?_ + ENNReal.ofReal (-x.log * x ^ (k + r) / (k + s + 1)) + + ENNReal.ofReal (x ^ (k + r) / (k + s + 1) ^ 2) := by + apply MeasureTheory.setLIntegral_congr_fun (by measurability) rintro x ⟨hx1, hx2⟩ + dsimp only rw [ENNReal.ofReal_add] · apply div_nonneg _ (by positivity) apply mul_nonneg _ (by apply pow_nonneg (by linarith)) @@ -649,10 +644,8 @@ lemma J_ENN_rs_eq_tsum_aux_intergal (r s k : ℕ): apply Real.log_nonpos (by nlinarith) (by nlinarith) · apply div_nonneg _ (by positivity) apply pow_nonneg (by linarith) - rw [h2, MeasureTheory.lintegral_add_left'] - · simp only [Set.mem_Ioo] at h2 - rw [aux_lintegral3 k r s, aux_lintegral4 k r s, ENNReal.ofReal_add] + · rw [aux_lintegral3 k r s, aux_lintegral4 k r s, ENNReal.ofReal_add] · apply div_nonneg (by norm_num) (by positivity) · apply div_nonneg (by norm_num) (by positivity) · apply AEMeasurable.ennreal_ofReal @@ -665,12 +658,12 @@ lemma J_ENN_rs_eq_tsum_aux_intergal (r s k : ℕ): · rw [MeasureTheory.Measure.prod_restrict, ← MeasureTheory.Measure.volume_eq_prod] exact AEMeasurable_aux' -lemma J_ENN_rs_eq_tsum (r s : ℕ) : J_ENN r s = ∑' (k : ℕ), ENNReal.ofReal +lemma J_ENN_rs_eq_tsum (r s : ℕ) : jENN r s = ∑' (k : ℕ), ENNReal.ofReal (1 / ((k + r + 1) ^ 2 * (k + s + 1)) + 1 / ((k + r + 1) * (k + s + 1) ^ 2)) := by calc _ = ∫⁻ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, ∑' (k : ℕ), ENNReal.ofReal (- (x.1 * x.2).log * x.1 ^ (k + r) * x.2 ^ (k + s)) := by - rw [J_ENN, ← MeasureTheory.lintegral_indicator (by measurability), + rw [jENN, ← MeasureTheory.lintegral_indicator (by measurability), ← MeasureTheory.lintegral_indicator (by measurability)] congr ext y @@ -711,9 +704,9 @@ lemma J_ENN_rs_eq_tsum (r s : ℕ) : J_ENN r s = ∑' (k : ℕ), ENNReal.ofReal (1 / ((k + r + 1) ^ 2 * (k + s + 1)) + 1 / ((k + r + 1) * (k + s + 1) ^ 2)) := by simp_rw [J_ENN_rs_eq_tsum_aux_intergal r s] -lemma J_ENN_rr (r : ℕ) : J_ENN r r = ENNReal.ofReal +lemma J_ENN_rr (r : ℕ) : jENN r r = ENNReal.ofReal (2 * ∑' n : ℕ , 1 / ((n : ℝ) + 1) ^ 3 - 2 * ∑ m ∈ Finset.Icc 1 r, 1 / (m : ℝ) ^ 3) := by - have h : J_ENN r r = ∑' (k : ℕ), ENNReal.ofReal (2 / ((k + r + 1) ^ 3)) := by + have h : jENN r r = ∑' (k : ℕ), ENNReal.ofReal (2 / ((k + r + 1) ^ 3)) := by rw [J_ENN_rs_eq_tsum r r] congr ext k @@ -724,13 +717,13 @@ lemma J_ENN_rr (r : ℕ) : J_ENN r r = ENNReal.ofReal 2 * ∑' n : ℕ , 1 / ((n : ℝ) + 1) ^ 3 - 2 * ∑ m ∈ Finset.Icc 1 r, 1 / (m : ℝ) ^ 3 := by symm apply sub_eq_of_eq_add - rw [← sum_add_tsum_nat_add' (k := r) (f := fun k => 1 / ((k : ℝ) + 1) ^ 3), mul_add, add_comm, - ← tsum_mul_left] - · simp only [mul_one_div, ← two_mul, ← mul_assoc, ← mul_add] + rw [← Summable.sum_add_tsum_nat_add' (k := r) (f := fun k => 1 / ((k : ℝ) + 1) ^ 3), + mul_add, add_comm, ← tsum_mul_left] + · simp only [mul_one_div] congr 1 · norm_cast · congr 1 - rw [← Nat.Ico_succ_right, Nat.succ_eq_add_one] + rw [← Finset.Ico_add_one_right_eq_Icc] have h1 := Finset.sum_Ico_eq_sum_range (m := 1) (n := r + 1) (f := fun k => 1 / (k : ℝ) ^ 3) simp only [add_tsub_cancel_right, Nat.cast_add, Nat.cast_one] at h1 simp only [h1, add_comm] @@ -746,13 +739,13 @@ lemma J_ENN_rr (r : ℕ) : J_ENN r r = ENNReal.ofReal simp only [add_assoc, Nat.cast_pow] rw [summable_nat_add_iff (k := r + 1) (f := fun k => 2 / (k ^ 3 : ℝ))] have h2 := Real.summable_one_div_nat_pow (p := 3) - simp only [Real.summable_nat_pow_inv, Nat.one_lt_ofNat] at h2 + simp only [Nat.one_lt_ofNat] at h2 apply Iff.symm at h2 rw [true_iff, ← summable_mul_left_iff (a := 2) (by norm_num)] at h2 simp only [mul_one_div] at h2 exact h2 -lemma fun_of_J_nonneg (r s: ℕ) (x : ℝ × ℝ) (hx : x ∈ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1) : +lemma fun_of_J_nonneg (r s : ℕ) (x : ℝ × ℝ) (hx : x ∈ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1) : 0 ≤ -Real.log (x.1 * x.2) / (1 - x.1 * x.2) * x.1 ^ r * x.2 ^ s := by simp only [Set.mem_prod, Set.mem_Ioo] at hx apply mul_nonneg @@ -770,7 +763,7 @@ lemma integrableOn_J_rr (r : ℕ) : MeasureTheory.IntegrableOn (fun x ↦ -Real.log (x.1 * x.2) / (1 - x.1 * x.2) * x.1 ^ r * x.2 ^ r) (Set.Ioo 0 1 ×ˢ Set.Ioo 0 1) MeasureTheory.volume := by have h := J_ENN_rr r - simp only [J_ENN] at h + simp only [jENN] at h rw [MeasureTheory.IntegrableOn, MeasureTheory.Integrable] constructor · apply AEMeasurable.aestronglyMeasurable @@ -811,17 +804,18 @@ lemma integrableOn_J_rr (r : ℕ) : MeasureTheory.IntegrableOn theorem J_rr (r : ℕ) : J r r = 2 * ∑' n : ℕ , 1 / ((n : ℝ) + 1) ^ 3 - 2 * ∑ m ∈ Finset.Icc 1 r, 1 / (m : ℝ) ^ 3 := by have h := J_ENN_rr r - simp only [J_ENN] at h + simp only [jENN] at h rw [J, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, h, ENNReal.toReal_ofReal_eq_iff] - · simp only [sub_nonneg, Nat.ofNat_pos, mul_le_mul_left] - rw [← Nat.Ico_succ_right, Nat.succ_eq_add_one] + · simp only [sub_nonneg] + apply mul_le_mul_of_nonneg_left ?_ (by norm_num) + rw [← Finset.Ico_add_one_right_eq_Icc] nth_rw 1 [← zero_add (a := 1)] rw [← Finset.sum_Ico_add' (c := 1)] norm_cast - apply sum_le_tsum + apply Summable.sum_le_tsum · intro i _; positivity · norm_cast - simp only [add_assoc, Nat.cast_pow] + simp only [Nat.cast_pow] rw [summable_nat_add_iff (k := 1) (f := fun k => 1 / (k ^ 3 : ℝ)), Real.summable_one_div_nat_pow (p := 3)] norm_num @@ -868,7 +862,7 @@ lemma summable_aux (r : ℕ) : Summable fun (b : ℕ) ↦ 1 / ((b : ℝ) + r + 1 norm_num lemma J_ENN_rs (r s : ℕ) (h : r > s) : - J_ENN r s = ENNReal.ofReal ((∑ k ∈ Finset.Ioc s r, 1 / (k : ℝ) ^ 2) / (r - s)) := by + jENN r s = ENNReal.ofReal ((∑ k ∈ Finset.Ioc s r, 1 / (k : ℝ) ^ 2) / (r - s)) := by calc _ = ∑' (k : ℕ), ENNReal.ofReal (1 / (r - s) * (1 / (k + s + 1) ^ 2 - 1 / (k + r + 1) ^ 2)) := by rw [J_ENN_rs_eq_tsum] @@ -906,15 +900,17 @@ lemma J_ENN_rs (r s : ℕ) (h : r > s) : rw [← ENNReal.ofReal_tsum_of_nonneg] · rw [ENNReal.ofReal_eq_ofReal_iff] · simp only [mul_sub] - · rw [tsum_sub] + · rw [Summable.tsum_sub] · simp only [sum_div, div_div, ← one_div_mul_one_div_rev] apply sub_eq_of_eq_add - rw [← sum_add_tsum_nat_add' (f := fun n => 1 / (r - s) * (1 / (n + (s : ℝ) + 1) ^ 2)) (k := r - s)] + rw [← Summable.sum_add_tsum_nat_add' + (f := fun n => 1 / (r - s) * (1 / (n + (s : ℝ) + 1) ^ 2)) (k := r - s)] · congr 1 · simp only [← Nat.cast_add, add_comm] rw [← Finset.sum_Ico_eq_sum_range (n := r) (m := s) - (f := fun k => 1 / (r - s) * (1 / ((k : ℝ) + 1) ^ 2)), ← Nat.Ico_succ_succ, - Nat.succ_eq_add_one, ← Finset.sum_Ico_add' (c := 1) (b := r) (a := s)] + (f := fun k => 1 / (r - s) * (1 / ((k : ℝ) + 1) ^ 2)), + ← Finset.Ico_add_one_add_one_eq_Ioc, + ← Finset.sum_Ico_add' (c := 1) (b := r) (a := s)] norm_cast · congr ext n @@ -954,7 +950,7 @@ lemma integrableOn_J_rs' (r s : ℕ) (h : r > s) : MeasureTheory.IntegrableOn (fun x ↦ -Real.log (x.1 * x.2) / (1 - x.1 * x.2) * x.1 ^ r * x.2 ^ s) (Set.Ioo 0 1 ×ˢ Set.Ioo 0 1) MeasureTheory.volume := by have h₀ := J_ENN_rs r s h - simp only [J_ENN] at h₀ + simp only [jENN] at h₀ rw [MeasureTheory.IntegrableOn, MeasureTheory.Integrable] constructor · apply AEMeasurable.aestronglyMeasurable @@ -995,7 +991,7 @@ lemma integrableOn_J_rs' (r s : ℕ) (h : r > s) : MeasureTheory.IntegrableOn lemma J_rs' (r s : ℕ) (h : r > s) : J r s = (∑ k ∈ Finset.Ioc s r, 1 / (k : ℝ) ^ 2) / (r - s) := by have h₀ := J_ENN_rs r s h - simp only [J_ENN] at h₀ + simp only [jENN] at h₀ rw [J, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, h₀, ENNReal.toReal_ofReal_eq_iff] · rw [sum_div] apply sum_nonneg @@ -1024,7 +1020,7 @@ lemma J_rs' (r s : ℕ) (h : r > s) : · apply Measurable.pow measurable_fst measurable_const · apply Measurable.pow measurable_snd measurable_const -lemma J_ENN_rs_symm (r s : ℕ) : J_ENN r s = J_ENN s r := by +lemma J_ENN_rs_symm (r s : ℕ) : jENN r s = jENN s r := by simp only [J_ENN_rs_eq_tsum, add_comm, mul_comm] lemma integrableOn_J_rs (r s : ℕ) : MeasureTheory.IntegrableOn @@ -1073,12 +1069,12 @@ lemma integrableOn_J_rs (r s : ℕ) : MeasureTheory.IntegrableOn · simp only [hx, ↓reduceIte] have h₀ := J_ENN_rs s r h2 rw [J_ENN_rs_symm s r] at h₀ - simp only [J_ENN] at h₀ + simp only [jENN] at h₀ rw [h1, h₀] simp only [one_div, ENNReal.ofReal_lt_top] -lemma J_eq_toReal_J_ENN (r s : ℕ) : J r s = (J_ENN r s).toReal := by - rw [J, J_ENN, MeasureTheory.integral_eq_lintegral_of_nonneg_ae] +lemma J_eq_toReal_J_ENN (r s : ℕ) : J r s = (jENN r s).toReal := by + rw [J, jENN, MeasureTheory.integral_eq_lintegral_of_nonneg_ae] · apply MeasureTheory.ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter · exact integrableOn_J_rs r s · rintro x hx - @@ -1105,16 +1101,16 @@ theorem J_rs {r s : ℕ} (h : r ≠ s) : J r s = (∑ m ∈ Icc 1 r, 1 / (m : ℝ) ^ 2 - ∑ m ∈ Icc 1 s, 1 / (m : ℝ) ^ 2) / (r - s) := by by_cases h1 : r > s · simp only [J_rs' r s h1, sub_div, sum_div] - rw [← Nat.Ico_succ_succ, Finset.sum_Ico_eq_sub] + rw [← Finset.Ico_add_one_add_one_eq_Ioc, Finset.sum_Ico_eq_sub] · congr 1 · rw [← Finset.sum_range_add_sum_Ico (n := r + 1) (m := 1) _ (by omega)] simp only [range_one, one_div, sum_singleton, CharP.cast_eq_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, inv_zero, zero_div, zero_add] - rw [ Nat.Ico_succ_right] + rw [ Finset.Ico_add_one_right_eq_Icc] · rw [← Finset.sum_range_add_sum_Ico (n := s + 1) (m := 1) _ (by omega)] simp only [range_one, one_div, sum_singleton, CharP.cast_eq_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, inv_zero, zero_div, zero_add] - rw [ Nat.Ico_succ_right] + rw [ Finset.Ico_add_one_right_eq_Icc] · linarith · simp only [gt_iff_lt, not_lt] at h1 have h2 : s > r := by @@ -1123,14 +1119,14 @@ theorem J_rs {r s : ℕ} (h : r ≠ s) : J r s = nth_rw 2 [← neg_div_neg_eq] simp only [neg_sub] congr 1 - rw [← Nat.Ico_succ_succ, Finset.sum_Ico_eq_sub] + rw [← Finset.Ico_add_one_add_one_eq_Ioc, Finset.sum_Ico_eq_sub] · congr 1 · rw [← Finset.sum_range_add_sum_Ico (n := s + 1) (m := 1) _ (by omega)] simp only [range_one, one_div, sum_singleton, CharP.cast_eq_zero, ne_eq, - OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, inv_zero, zero_div, zero_add] - rw [ Nat.Ico_succ_right] + OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, inv_zero, zero_add] + rw [ Finset.Ico_add_one_right_eq_Icc] · rw [← Finset.sum_range_add_sum_Ico (n := r + 1) (m := 1) _ (by omega)] simp only [range_one, one_div, sum_singleton, CharP.cast_eq_zero, ne_eq, - OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, inv_zero, zero_div, zero_add] - rw [ Nat.Ico_succ_right] + OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, inv_zero, zero_add] + rw [ Finset.Ico_add_one_right_eq_Icc] · linarith diff --git a/Zeta3Irrational/LegendrePoly.lean b/Zeta3Irrational/LegendrePoly.lean index d682b28..9541b4c 100644 --- a/Zeta3Irrational/LegendrePoly.lean +++ b/Zeta3Irrational/LegendrePoly.lean @@ -1,16 +1,18 @@ -import Mathlib.Algebra.Lie.OfAssociative import Mathlib.Algebra.Polynomial.Derivative import Mathlib.Algebra.Polynomial.Eval.SMul +import Mathlib.RingTheory.Polynomial.ShiftedLegendre import Mathlib.Analysis.Calculus.Deriv.Inv import Mathlib.Analysis.Calculus.Deriv.Pow -import Mathlib.Data.Real.StarOrdered -import Mathlib.MeasureTheory.Integral.IntegrationByParts +import Mathlib.Analysis.Calculus.Deriv.Polynomial +import Mathlib.Analysis.Real.Sqrt +import Mathlib.Topology.Algebra.Polynomial +import Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts /-! # Legendre Polynomials -In this file, we define the shiftedLegendre polynomials `shiftedLegendre n` for `n : ℕ` as a -polynomial in `ℤ[X]`. We prove some basic properties of the shiftedLegendre polynomials. +We use the real shifted Legendre polynomials `aperyShiftedLegendre n` for `n : ℕ` as +a polynomial in `ℝ[X]`. We prove some basic properties of the aperyShiftedLegendre polynomials. -/ @@ -21,71 +23,42 @@ variable {R : Type*} namespace Polynomial -/-- `shiftedLegendre n` is the polynomial defined in terms of derivatives of order n. -/ -noncomputable def shiftedLegendre (n : ℕ) : ℝ[X] := - C (n ! : ℝ)⁻¹ * derivative^[n] (X ^ n * (1 - X) ^ n) +/-- The real shifted Legendre polynomial, obtained from Mathlib's integer polynomial. -/ +noncomputable def aperyShiftedLegendre (n : ℕ) : ℝ[X] := + (shiftedLegendre n).map (Int.castRingHom ℝ) + +/-- The canonical polynomial has exactly the Rodrigues normalization used in the source. -/ +lemma aperyShiftedLegendre_eq_rodrigues (n : ℕ) : + aperyShiftedLegendre n = C (n ! : ℝ)⁻¹ * derivative^[n] (X ^ n * (1 - X) ^ n) := by + have h := congrArg (Polynomial.map (Int.castRingHom ℝ)) + (factorial_mul_shiftedLegendre_eq n) + have h' : C (n ! : ℝ) * aperyShiftedLegendre n = + derivative^[n] (X ^ n * (1 - X) ^ n) := by + simpa only [aperyShiftedLegendre, Polynomial.map_mul, Polynomial.map_natCast, + ← iterate_derivative_map, Polynomial.map_pow, Polynomial.map_sub, + Polynomial.map_one, Polynomial.map_X, C_eq_natCast] using h + rw [← h', ← mul_assoc, ← C_mul, inv_mul_cancel₀ (by positivity), C_1, one_mul] lemma Finsum_iterate_deriv [CommRing R] (k : ℕ) (h : ℕ → ℕ) : derivative^[k] (∑ m ∈ Finset.range (k + 1), (h m) • ((-1) ^ m : R[X]) * X ^ (k + m)) = ∑ m ∈ Finset.range (k + 1), (h m) • (-1) ^ m * derivative^[k] (X ^ (k + m)) := by - induction' k + 1 with n hn - · simp only [Nat.zero_eq, Finset.range_zero, Finset.sum_empty, iterate_map_zero] - · rw[Finset.sum_range, Finset.sum_range, Fin.sum_univ_castSucc, Fin.sum_univ_castSucc] at * - simp only [Fin.coe_castSucc, Fin.val_last, iterate_map_add, hn, add_right_inj] - rw [nsmul_eq_mul, mul_assoc, ← nsmul_eq_mul, Polynomial.iterate_derivative_smul, nsmul_eq_mul, - mul_assoc] - rcases n.even_or_odd with (hn1 | hn2) - · simp_all only [nsmul_eq_mul, Int.even_coe_nat, Even.neg_pow, one_pow, one_mul] - · rw [Odd.neg_one_pow] - simp only [neg_mul, one_mul, iterate_map_neg, mul_neg] - exact_mod_cast hn2 + simp only [iterate_derivative_sum] + congr! 1 with m _ + rw [show (h m) • ((-1) ^ m : R[X]) = C ((h m : R) * (-1) ^ m) by simp, + iterate_derivative_C_mul] -/-- The expand of `shiftedLegendre n`. -/ -theorem shiftedLegendre_eq_sum (n : ℕ) : shiftedLegendre n = ∑ k ∈ Finset.range (n + 1), - C ((-1) ^ k : ℝ) * (Nat.choose n k : ℝ[X]) * (Nat.choose (n + k) n : ℝ[X]) * X ^ k := by - have h : ((X : ℝ[X]) - X ^ 2) ^ n = - ∑ m ∈ range (n + 1), n.choose m • (- 1) ^ m * X ^ (n + m) := by - rw[sub_eq_add_neg, add_comm, add_pow] - congr! 1 with m hm - rw[neg_pow, pow_two, mul_pow,← mul_assoc, mul_comm, mul_assoc, pow_mul_pow_sub, mul_assoc, - ← pow_add, ← mul_assoc, nsmul_eq_mul, add_comm] - rw[Finset.mem_range] at hm - linarith - rw [shiftedLegendre, ← mul_pow, mul_one_sub, ← pow_two, h, Finsum_iterate_deriv, - Finset.mul_sum] - congr! 1 with x _ - rw [← mul_assoc, Polynomial.iterate_derivative_X_pow_eq_smul, Nat.descFactorial_eq_div - (by omega), show n + x - n = x by omega, nsmul_eq_mul, ← mul_assoc, mul_assoc, - mul_comm] - simp only [Int.reduceNeg, map_pow, map_neg, map_one] - rw [Algebra.smul_def, algebraMap_eq, map_natCast, ← mul_assoc, ← mul_assoc, add_comm, - Nat.add_choose, mul_assoc, mul_assoc, mul_assoc, mul_assoc, mul_assoc, mul_comm] - nth_rewrite 5 [mul_comm] - congr 1 - nth_rewrite 2 [mul_comm] - rw [← mul_assoc, ← mul_assoc, ← mul_assoc] - congr 1 - nth_rewrite 3 [mul_comm] - congr 1 - apply Polynomial.ext - intro m - simp only [one_div, coeff_mul_C, coeff_natCast_ite, Nat.cast_ite, CharP.cast_eq_zero, ite_mul, - zero_mul] - by_cases h : m = 0 - · simp [h] - rw [Nat.cast_div] - · rw [← one_div, ← div_mul_eq_div_mul_one_div] - norm_cast - rw [Nat.cast_div] - · exact Nat.factorial_mul_factorial_dvd_factorial_add x n - · norm_cast - apply mul_ne_zero (Nat.factorial_ne_zero x) (Nat.factorial_ne_zero n) - · exact Nat.factorial_dvd_factorial (by omega) - · norm_cast; exact Nat.factorial_ne_zero x - · simp only [h, ↓reduceIte] +/-- The expand of `aperyShiftedLegendre n`. -/ +theorem shiftedLegendre_eq_sum (n : ℕ) : aperyShiftedLegendre n = + ∑ k ∈ Finset.range (n + 1), + C ((-1) ^ k : ℝ) * (Nat.choose n k : ℝ[X]) * + (Nat.choose (n + k) n : ℝ[X]) * X ^ k := by + simp only [aperyShiftedLegendre, shiftedLegendre, Polynomial.map_sum, + Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_X, + map_mul, map_pow, map_neg, map_one, map_natCast, + Polynomial.map_neg, Polynomial.map_one, Polynomial.map_natCast] -/-- `shiftedLegendre n` is an integer polynomial. -/ -lemma shiftedLegendre_eq_int_poly (n : ℕ) : ∃ a : ℕ → ℤ, shiftedLegendre n = +/-- `aperyShiftedLegendre n` is an integer polynomial. -/ +lemma shiftedLegendre_eq_int_poly (n : ℕ) : ∃ a : ℕ → ℤ, aperyShiftedLegendre n = ∑ k ∈ Finset.range (n + 1), (a k : ℝ[X]) * X ^ k := by simp_rw [shiftedLegendre_eq_sum] use fun k => (- 1) ^ k * (Nat.choose n k) * (Nat.choose (n + k) n) @@ -99,40 +72,14 @@ lemma deriv_one_sub_X {n i : ℕ} : (⇑derivative)^[i] ((1 - X) ^ n : ℝ[X]) = Polynomial.iterate_derivative_X_pow_eq_smul, Algebra.smul_def, algebraMap_eq, map_natCast] simp -/-- The values ​​of the shiftedLegendre polynomial at x and 1-x differ by a factor (-1)ⁿ. -/ --- lemma shiftedLegendre_eval_symm (n : ℕ) (x : ℝ) : --- eval x (shiftedLegendre n) = (-1) ^ n * eval (1 - x) (shiftedLegendre n) := by --- rw [mul_comm] --- simp only [shiftedLegendre, eval_mul, one_div, eval_C] --- rw [mul_assoc] --- simp only [mul_eq_mul_left_iff, inv_eq_zero, Nat.cast_eq_zero]; left --- rw [Polynomial.iterate_derivative_mul] --- simp only [Nat.succ_eq_add_one, nsmul_eq_mul] --- rw [Polynomial.eval_finset_sum, Polynomial.eval_finset_sum, ← Finset.sum_flip, Finset.sum_mul] --- congr! 1 with i hi --- simp only [Polynomial.iterate_derivative_X_pow_eq_smul, eval_mul, eval_natCast, --- Algebra.smul_mul_assoc, eval_smul, eval_mul, eval_pow, eval_X, smul_eq_mul] --- simp only [Finset.mem_range, Nat.lt_add_one_iff] at hi --- rw [Nat.choose_symm hi, deriv_one_sub_X, deriv_one_sub_X] --- simp only [nsmul_eq_mul, eval_mul, eval_pow, eval_neg, eval_one, eval_natCast, eval_sub, eval_X, --- sub_sub_cancel] --- rw [mul_assoc] --- simp only [mul_eq_mul_left_iff, Nat.cast_eq_zero]; left --- rw [show n - (n - i) = i by omega, ← mul_assoc, ← mul_assoc, mul_comm, ← mul_assoc] --- symm --- rw [← mul_assoc] --- nth_rewrite 4 [mul_comm] --- rw [← mul_assoc, ← mul_assoc, mul_assoc] --- congr 1 --- rw [← pow_add, show i + n = n - i + 2 * i by omega, pow_add] --- simp only [even_two, Even.mul_right, Even.neg_pow, one_pow, mul_one] - theorem differentiableAt_inv_special {x a : ℝ} {n : ℕ} (ha : a > 0) (hx : 1 - a * x = 0) : ¬DifferentiableAt ℝ (fun x ↦ ↑n ! * a ^ n / (1 - a * x) ^ (n + 1)) x := by intro h obtain q := h.continuousAt - simp [Metric.continuousAt_iff, Real.dist_eq, hx] at q + simp only [Metric.continuousAt_iff, gt_iff_lt, Real.dist_eq, hx, ne_eq, + Nat.add_eq_zero_iff, one_ne_zero, and_false, not_false_eq_true, zero_pow, div_zero, + dist_zero_right, norm_div, norm_mul, RCLike.norm_natCast, norm_pow, Real.norm_eq_abs] at q have h₁ : ↑n ! * |a| ^ n > 0 := by apply mul_pos · simp only [Nat.cast_pos] @@ -150,19 +97,20 @@ theorem differentiableAt_inv_special {x a : ℝ} {n : ℕ} suffices 0 < q * a * q by linarith exact mul_pos (mul_pos qq ha) qq _ < 1 / 2 * q := by - rw [mul_lt_mul_right (a := q) qq] + rw [mul_lt_mul_iff_left₀ qq] linarith _ < q := by linarith specialize qqq this rw [div_lt_iff₀] at qqq · have : 1 < |1 - a * (a * q / 2 * q + x)| ^ (n + 1) := by - rwa [← mul_lt_mul_left (a := ↑n ! * |a| ^ n) h₁, mul_one] + rwa [← mul_lt_mul_iff_right₀ h₁, mul_one] rw [mul_add, add_comm, ← sub_sub, hx, zero_sub, abs_neg] at this have : |a * (a * q / 2 * q)| ^ (n + 1) < 1 := by - apply pow_lt_one₀ (by simp) _ (by omega) + apply pow_lt_one₀ (abs_nonneg _) _ (by omega) · nth_rewrite 2 [mul_comm] rw [← mul_assoc, ← mul_div_assoc, ← pow_two] - rw [show |((a * q) ^ 2 / 2 : ℝ)| = ((a * q) ^ 2 / 2 : ℝ) by exact abs_eq_self.2 (by positivity)] + rw [show |((a * q) ^ 2 / 2 : ℝ)| = ((a * q) ^ 2 / 2 : ℝ) by + exact abs_eq_self.2 (by positivity)] trans 1 / 2 · rw [div_lt_div_iff_of_pos_right (by norm_num), ← one_pow (n := 2)] apply pow_lt_pow_left₀ <;> nlinarith @@ -175,13 +123,13 @@ theorem differentiableAt_inv_special {x a : ℝ} {n : ℕ} rw [← mul_assoc, ← mul_div_assoc, ← pow_two] positivity · have : |q / 2 + x - x| < q := by - simp only [one_div, add_sub_cancel_right] + simp only [add_sub_cancel_right] rw [show |(q / 2 : ℝ)| = (q / 2 : ℝ) by exact abs_eq_self.2 (by linarith)] linarith specialize qqq this rw [div_lt_iff₀] at qqq · have : 1 < |1 - a * (q / 2 + x)| ^ (n + 1) := by - rwa [← mul_lt_mul_left (a := ↑n ! * |a| ^ n) h₁, mul_one] + rwa [← mul_lt_mul_iff_right₀ h₁, mul_one] rw [mul_add, add_comm, ← sub_sub, hx, zero_sub, abs_neg, ← mul_div_assoc, h2] at this have : 1 < (1 / 2 : ℝ) := by suffices (1 : ℝ) ≥ |(1 / 2 : ℝ)| ^ (n + 1) by linarith @@ -192,8 +140,7 @@ theorem differentiableAt_inv_special {x a : ℝ} {n : ℕ} rw [abs_pos] linarith · have : |1 / a + x - x| < q := by - simp only [one_div, add_sub_cancel_right] - rw [← one_div] + simp only [add_sub_cancel_right] have : |(1 / a : ℝ)| = (1 / a : ℝ) := by rw [abs_eq_self, one_div_nonneg] linarith @@ -201,7 +148,7 @@ theorem differentiableAt_inv_special {x a : ℝ} {n : ℕ} specialize qqq this rw [div_lt_iff₀] at qqq · have : 1 < |1 - a * (1 / a + x)| ^ (n + 1) := by - rwa [← mul_lt_mul_left (a := ↑n ! * |a| ^ n) h₁, mul_one] + rwa [← mul_lt_mul_iff_right₀ h₁, mul_one] rw [mul_add, add_comm, ← sub_sub, hx, zero_sub, abs_neg, ← mul_div_assoc, mul_one, div_self (by linarith)] at this simp only [abs_one, one_pow, lt_self_iff_false] at this @@ -211,20 +158,20 @@ theorem differentiableAt_inv_special {x a : ℝ} {n : ℕ} lemma n_derivative {a : ℝ} (n : ℕ) (ha : a > 0) : deriv^[n] (fun x ↦ 1 / (1 - a * x)) = fun x ↦ (n) ! * (a ^ n) / (1 - a * x) ^ (n + 1) := by - induction' n with n hn - · simp - · ext x + induction n with + | zero => simp + | succ n hn => + ext x rcases eq_or_ne (1 - a * x) 0 with (h | hne) · simp only [h, ne_eq, add_eq_zero, one_ne_zero, and_false, not_false_eq_true, zero_pow, div_zero] rw [Function.iterate_succ_apply', hn] apply deriv_zero_of_not_differentiableAt exact differentiableAt_inv_special ha h - · rw [Function.iterate_succ_apply', hn, deriv_div] - · simp only [differentiableAt_const, deriv_mul, deriv_const', zero_mul, deriv_pow'', - mul_zero, add_zero, zero_sub] + · rw [Function.iterate_succ_apply', hn, deriv_fun_div] + · simp only [deriv_const', zero_mul, zero_sub] rw [div_eq_div_iff] - · rw [deriv_pow'', deriv_const_sub, deriv_const_mul] + · rw [deriv_fun_pow, deriv_const_sub, deriv_const_mul] · simp only [Nat.cast_add, Nat.cast_one, add_tsub_cancel_right, deriv_id'', mul_one, mul_neg, neg_neg] norm_cast @@ -253,7 +200,9 @@ theorem differentiableAt_inv_special' (c x y z : ℝ) (n : ℕ) (hc : c ≠ 0) ( ¬DifferentiableAt ℝ (fun y ↦ c / (1 - (1 - x * y) * z) ^ (n + 1)) y := by intro h obtain q := h.continuousAt - simp [Metric.continuousAt_iff, Real.dist_eq, h1] at q + simp only [Metric.continuousAt_iff, gt_iff_lt, Real.dist_eq, h1, ne_eq, + Nat.add_eq_zero_iff, one_ne_zero, and_false, not_false_eq_true, zero_pow, div_zero, + dist_zero_right, norm_div, Real.norm_eq_abs, norm_pow] at q simp only [Set.mem_Ioo] at hx hz have h₁ : |c| > 0 := by simp [hc] specialize q (|c|) h₁ @@ -270,9 +219,9 @@ theorem differentiableAt_inv_special' (c x y z : ℝ) (n : ℕ) (hc : c ≠ 0) ( exact min_le_left (q / 2) (1 / |x * z|) have hd' : 1 - (1 - x * d) * z ≠ 0 := by suffices 1 - (1 - x * d) * z > 0 by linarith - rw [h', show 1 - (1 - x * (d' + y)) * z = 1 - (1 - x * y) * z + x * z * d' by ring, h1, zero_add] - apply mul_pos - apply mul_pos (by linarith) (by linarith) + rw [h', show 1 - (1 - x * (d' + y)) * z = + 1 - (1 - x * y) * z + x * z * d' by ring, h1, zero_add] + refine mul_pos (mul_pos (by linarith) (by linarith)) ?_ simp only [d'] apply lt_min (by positivity) simp only [one_div, inv_pos, abs_pos, ne_eq, mul_eq_zero, not_or] @@ -290,9 +239,8 @@ theorem differentiableAt_inv_special' (c x y z : ℝ) (n : ℕ) (hc : c ≠ 0) ( rw [← abs_one_div] apply abs_le_abs_of_nonneg (by positivity) simp only [d'] - rw [abs_of_nonneg (a := x * z)] + rw [abs_of_nonneg (mul_nonneg (by linarith) (by linarith) : 0 ≤ x * z)] exact min_le_right (q / 2) (1 / (x * z)) - exact mul_nonneg (by linarith) (by linarith) _ = 1 := by rw [mul_div, mul_one, div_self] simp only [ne_eq, abs_eq_zero, mul_eq_zero, not_or] @@ -305,13 +253,14 @@ theorem differentiableAt_inv_special' (c x y z : ℝ) (n : ℕ) (hc : c ≠ 0) ( lemma n_derivative' {x z : ℝ} (n : ℕ) (hx : x ∈ Set.Ioo 0 1) (hz : z ∈ Set.Ioo 0 1) : (deriv^[n] fun y ↦ 1 / (1 - (1 - x * y) * z)) = (fun y ↦ (-1) ^ n * (n) ! * (x * z) ^ n / (1 - (1 - x * y) * z) ^ (n + 1)) := by - induction' n with n hn - · simp - · ext y + induction n with + | zero => simp + | succ n hn => + ext y rcases eq_or_ne (1 - (1 - x * y) * z) 0 with (h | hne) · simp only [h, ne_eq, add_eq_zero, one_ne_zero, and_false, not_false_eq_true, zero_pow, div_zero] - simp only [Set.mem_Ioo, Set.mem_Icc] at hx hz + simp only [Set.mem_Ioo] at hx hz rw [Function.iterate_succ_apply', hn] apply deriv_zero_of_not_differentiableAt set c := (-1) ^ n * ↑n ! * (x * z) ^ n @@ -323,17 +272,18 @@ lemma n_derivative' {x z : ℝ} (n : ℕ) (hx : x ∈ Set.Ioo 0 1) (hz : z ∈ S · apply pow_ne_zero nlinarith exact differentiableAt_inv_special' c x y z n hc hx hz h - · rw [Function.iterate_succ_apply', hn, deriv_div] - · simp only [differentiableAt_const, deriv_mul, deriv_const', zero_mul, deriv_pow'', - mul_zero, add_zero, zero_sub] - have h : (fun y ↦ (1 - (1 - x * y) * z) ^ (n + 1)) = fun y ↦ (1 - z + x * z * y) ^ (n + 1) := by + · rw [Function.iterate_succ_apply', hn, deriv_fun_div] + · simp only [deriv_const', zero_mul, zero_sub] + have h : (fun y ↦ (1 - (1 - x * y) * z) ^ (n + 1)) = + fun y ↦ (1 - z + x * z * y) ^ (n + 1) := by ext _; ring rw [div_eq_div_iff] - · rw [h, deriv_pow'', deriv_const_add, deriv_const_mul] + · rw [h, deriv_fun_pow, deriv_const_add, deriv_const_mul] · simp only [Nat.cast_add, Nat.cast_one, add_tsub_cancel_right, deriv_id'', mul_one, ← neg_mul] rw [show -(-1) ^ n = (-1 : ℝ) ^ (n + 1) by ring, - show ((n + 1)! : ℝ) = (((n : ℕ) + 1) : ℝ) * (n !) by rw [Nat.factorial_succ]; norm_cast] + show ((n + 1)! : ℝ) = (((n : ℕ) + 1) : ℝ) * (n !) by + rw [Nat.factorial_succ]; norm_cast] ring · apply differentiableAt_id · apply DifferentiableAt.add @@ -352,16 +302,17 @@ lemma n_derivative' {x z : ℝ} (n : ℕ) (hx : x ∈ Set.Ioo 0 1) (hz : z ∈ S apply DifferentiableAt.const_mul differentiableAt_id · exact pow_ne_zero (n + 1) hne -lemma shiftedLegendre_poly_eval_zero_eq_zero {m : ℕ} (h : m < n) : +lemma shiftedLegendre_poly_eval_zero_eq_zero {n m : ℕ} (h : m < n) : eval 0 ((⇑derivative)^[m] (X ^ n * (1 - X) ^ n) : ℝ[X]) = 0 := by - rw [Polynomial.iterate_derivative_mul, Polynomial.eval_finset_sum] + rw [Polynomial.iterate_derivative_mul, Polynomial.eval_finsetSum] apply Finset.sum_eq_zero intro x hx simp_all only [Nat.succ_eq_add_one, Finset.mem_range, nsmul_eq_mul, eval_mul, eval_natCast, mul_eq_zero, Nat.cast_eq_zero] right; left simp only [Polynomial.iterate_derivative_X_pow_eq_smul, eval_smul, eval_pow, eval_X, smul_eq_mul, - mul_eq_zero, Nat.cast_eq_zero, Nat.descFactorial_eq_zero_iff_lt, pow_eq_zero_iff', ne_eq, true_and] + mul_eq_zero, Nat.cast_eq_zero, Nat.descFactorial_eq_zero_iff_lt, pow_eq_zero_iff', + ne_eq, true_and] right suffices n - (m - x) > 0 by linarith simp only [gt_iff_lt, tsub_pos_iff_lt] @@ -370,9 +321,9 @@ lemma shiftedLegendre_poly_eval_zero_eq_zero {m : ℕ} (h : m < n) : m - x ≤ m := by simp _ < n := by exact h -lemma shiftedLegendre_poly_eval_one_eq_zero {m : ℕ} (h : m < n) : +lemma shiftedLegendre_poly_eval_one_eq_zero {n m : ℕ} (h : m < n) : eval 1 ((⇑derivative)^[m] (X ^ n * (1 - X) ^ n) : ℝ[X]) = 0 := by - rw [Polynomial.iterate_derivative_mul, Polynomial.eval_finset_sum] + rw [Polynomial.iterate_derivative_mul, Polynomial.eval_finsetSum] apply Finset.sum_eq_zero intro x hx simp_all only [Nat.succ_eq_add_one, Finset.mem_range, nsmul_eq_mul, eval_mul, eval_natCast, @@ -391,29 +342,11 @@ lemma shiftedLegendre_poly_eval_one_eq_zero {m : ℕ} (h : m < n) : linarith lemma shiftedLegendre_continuousOn {n m : ℕ} : ContinuousOn - (fun x ↦ eval x ((⇑derivative)^[n - m] (X ^ n * (1 - X) ^ n : ℝ[X]))) (Set.uIcc 0 1) := by - simp_rw [Polynomial.iterate_derivative_mul, Polynomial.eval_finset_sum] - apply continuousOn_finset_sum - intro i _ - simp_rw [Algebra.smul_def, eval_mul] - apply ContinuousOn.mul - · simp only [eq_natCast, eval_natCast, ge_iff_le, zero_le_one, Set.uIcc_of_le] - apply continuousOn_const - · apply ContinuousOn.mul - · simp_rw [Polynomial.iterate_derivative_X_pow_eq_smul] - simp only [eval_smul, eval_pow, eval_X, smul_eq_mul, ge_iff_le, zero_le_one, - Set.uIcc_of_le] - apply ContinuousOn.mul continuousOn_const (ContinuousOn.pow continuousOn_id _) - · rw [show (1 - X : ℝ[X]) ^ n = (X ^ n : ℝ[X]).comp (1 - X) by simp, - Polynomial.iterate_derivative_comp_one_sub_X (p := X ^ n), - Polynomial.iterate_derivative_X_pow_eq_smul] - simp only [smul_comp, pow_comp, X_comp, Algebra.mul_smul_comm, eval_smul, eval_mul, - eval_pow, eval_neg, eval_one, eval_sub, eval_X, smul_eq_mul, ge_iff_le, zero_le_one, - Set.uIcc_of_le] - refine ContinuousOn.mul continuousOn_const (ContinuousOn.mul continuousOn_const ?_) - apply ContinuousOn.pow (ContinuousOn.sub continuousOn_const continuousOn_id) + (fun x ↦ eval x ((⇑derivative)^[n - m] (X ^ n * (1 - X) ^ n : ℝ[X]))) (Set.uIcc 0 1) := + (Polynomial.continuous _).continuousOn -lemma special_deriv_div_continuousOn {m : ℕ} {x z: ℝ} (hx : x ∈ Set.Ioo 0 1) (hz : z ∈ Set.Ioo 0 1) : +lemma special_deriv_div_continuousOn {m : ℕ} {x z : ℝ} + (hx : x ∈ Set.Ioo 0 1) (hz : z ∈ Set.Ioo 0 1) : ContinuousOn (fun u ↦ (deriv^[m] fun y ↦ 1 / (1 - (1 - x * y) * z)) u) (Set.uIcc 0 1) := by simp_rw [n_derivative' m hx hz] apply ContinuousOn.div continuousOn_const @@ -437,58 +370,26 @@ lemma integral_shiftedLegendre_mul_smooth_eq_aux {x z : ℝ} (n m : ℕ) (h : m eval y ((⇑derivative)^[n] (X ^ n * (1 - X) ^ n)) * (fun y ↦ 1 / (1 - (1 - x * y) * z)) y = (- 1) ^ m * ∫ (y : ℝ) in (0)..1, eval y ((⇑derivative)^[n - m] (X ^ n * (1 - X) ^ n)) * (deriv^[m] fun y ↦ 1 / (1 - (1 - x * y) * z)) y:= by - induction' m with m hm - · simp - · have h₀ : m < n := by linarith + induction m with + | zero => simp + | succ m hm => + have h₀ : m < n := by linarith have h₁ : n - (m + 1) < n := by omega rw [hm (LT.lt.le h₀), pow_add, pow_one, mul_assoc] congr symm rw [show n - m = n - (m + 1) + 1 by omega, Function.iterate_succ_apply'] - rw [neg_one_mul, neg_eq_iff_eq_neg, intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDerivAt + rw [neg_one_mul, neg_eq_iff_eq_neg, + intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDerivAt (u := fun u ↦ eval u ((⇑derivative)^[n - (m + 1)] (X ^ n * (1 - X) ^ n : ℝ[X]))) (u' := fun u ↦ eval u (derivative ((⇑derivative)^[n - (m + 1)] (X ^ n * (1 - X) ^ n : ℝ[X])))) (v := fun u ↦ (deriv^[m] fun y ↦ 1 / (1 - (1 - x * y) * z)) u)] · rw [shiftedLegendre_poly_eval_one_eq_zero h₁, shiftedLegendre_poly_eval_zero_eq_zero h₁] - simp only [one_mul, one_div, zero_mul, sub_zero, sub_self, zero_sub, - Function.iterate_succ_apply', neg_inj] + simp only [one_div, zero_mul, sub_self, zero_sub, Function.iterate_succ_apply'] · apply shiftedLegendre_continuousOn · apply special_deriv_div_continuousOn hx hz - · intro x _ - simp_rw [Polynomial.iterate_derivative_mul, Polynomial.eval_finset_sum] - simp only [Nat.succ_eq_add_one, nsmul_eq_mul, eval_mul, eval_natCast, map_sum, eval_finset_sum] - apply HasDerivAt.sum - intro i _ - simp only [derivative_mul, derivative_natCast, zero_mul, zero_add, eval_mul, eval_natCast, - eval_add] - apply HasDerivAt.const_mul - apply HasDerivAt.mul - · rw [Polynomial.iterate_derivative_X_pow_eq_smul] - simp only [eval_smul, eval_pow, eval_X, smul_eq_mul, LinearMapClass.map_smul, - derivative_X_pow, map_natCast, eval_mul, eval_natCast] - apply HasDerivAt.const_mul - apply hasDerivAt_pow - · rw [show (1 - X : ℝ[X]) ^ n = (X ^ n : ℝ[X]).comp (1 - X) by simp, - Polynomial.iterate_derivative_comp_one_sub_X (p := X ^ n), - Polynomial.iterate_derivative_X_pow_eq_smul] - simp only [smul_comp, pow_comp, X_comp, Algebra.mul_smul_comm, eval_smul, eval_mul, - eval_pow, eval_neg, eval_one, eval_sub, eval_X, smul_eq_mul, LinearMapClass.map_smul] - apply HasDerivAt.const_mul - simp only [derivative_mul, eval_add, eval_mul, eval_pow, eval_sub, eval_one, eval_X, - eval_neg] - have h1 : (derivative ((-1) ^ i : ℝ[X])) = 0 := by - rw [show ((-1) ^ i : ℝ[X]) = C ((-1) ^ i) by simp, derivative_C] - rw [h1, eval_zero, zero_mul, zero_add] - apply HasDerivAt.const_mul - rw [show (1 - X : ℝ[X]) ^ (n - i) = (X ^ (n - i) : ℝ[X]).comp (1 - X) by simp, - Polynomial.derivative_comp_one_sub_X (p := X ^ (n - i)), - Polynomial.derivative_X_pow] - simp only [mul_comp, pow_comp, X_comp, eval_mul, map_natCast, natCast_comp, eval_neg, - eval_mul, eval_natCast, eval_pow, eval_sub, eval_one, eval_X] - rw [← mul_neg_one] - apply HasDerivAt.pow - apply HasDerivAt.const_sub - apply hasDerivAt_id + · intro u _ + exact Polynomial.hasDerivAt _ u · intro y hy simp only [Set.mem_Ioo, zero_le_one, min_eq_left, max_eq_right] at hx hy hz have hh : 1 - (1 - x * y) * z ≠ 0 := by @@ -502,7 +403,8 @@ lemma integral_shiftedLegendre_mul_smooth_eq_aux {x z : ℝ} (n m : ℕ) (h : m Function.eval u (deriv (deriv^[m] fun y ↦ 1 / (1 - (1 - x * y) * z))) := by simp only [one_div, Function.eval] simp_rw [this] - simp_rw [← Function.iterate_succ_apply', Nat.succ_eq_add_one, Function.eval, n_derivative' _ hx hz] + simp_rw [← Function.iterate_succ_apply', Nat.succ_eq_add_one, Function.eval, + n_derivative' _ hx hz] have : (-1) ^ (m + 1) * ↑(m + 1)! * (x * z) ^ (m + 1) / (1 - (1 - x * y) * z) ^ (m + 1 + 1) = (0 * (1 - (1 - x * y) * z) ^ (m + 1) - (-1) ^ m * ↑m ! * (x * z) ^ m * ((m + 1) * (x * z) * (1 - (1 - x * y) * z) ^ m)) / @@ -519,14 +421,16 @@ lemma integral_shiftedLegendre_mul_smooth_eq_aux {x z : ℝ} (n m : ℕ) (h : m rw [this] apply HasDerivAt.div · apply hasDerivAt_const - · have : (↑m + 1) * (x * z) * (1 - (1 - x * y) * z) ^ m = deriv (fun y ↦ (1 - (1 - x * y) * z) ^ (m + 1)) y := by + · have : (↑m + 1) * (x * z) * (1 - (1 - x * y) * z) ^ m = + deriv (fun y ↦ (1 - (1 - x * y) * z) ^ (m + 1)) y := by simp only [show 1 - (1 - x * y) * z = 1 - z + x * z * y by ring] - rw [deriv_pow'', show (fun y ↦ 1 - (1 - x * y) * z) = (fun y ↦ 1 - z + x * z * y) by ext _; ring] - · rw[deriv_const_add, deriv_const_mul] + rw [deriv_fun_pow, show (fun y ↦ 1 - (1 - x * y) * z) = + (fun y ↦ 1 - z + x * z * y) by ext _; ring] + · rw [deriv_const_add, deriv_const_mul] · simp only [Nat.cast_add, Nat.cast_one, add_tsub_cancel_right, deriv_id'', mul_one] norm_cast ring - · exact differentiableAt_id' + · exact differentiableAt_id · apply DifferentiableAt.const_sub apply DifferentiableAt.mul_const · apply DifferentiableAt.const_sub @@ -538,24 +442,7 @@ lemma integral_shiftedLegendre_mul_smooth_eq_aux {x z : ℝ} (n m : ℕ) (h : m · apply DifferentiableAt.const_sub apply DifferentiableAt.const_mul differentiableAt_id · apply pow_ne_zero _ hh - · simp_rw [← Function.iterate_succ_apply', Polynomial.iterate_derivative_mul, Polynomial.eval_finset_sum] - simp only [Nat.succ_eq_add_one, nsmul_eq_mul, eval_mul, eval_natCast] - apply ContinuousOn.intervalIntegrable_of_Icc (by norm_num) - apply continuousOn_finset_sum - intro i _ - apply ContinuousOn.mul continuousOn_const - · apply ContinuousOn.mul - · simp_rw [Polynomial.iterate_derivative_X_pow_eq_smul] - simp only [eval_smul, eval_pow, eval_X, smul_eq_mul] - apply ContinuousOn.mul continuousOn_const (ContinuousOn.pow continuousOn_id _) - · rw [show (1 - X : ℝ[X]) ^ n = (X ^ n : ℝ[X]).comp (1 - X) by simp, - Polynomial.iterate_derivative_comp_one_sub_X (p := X ^ n), - Polynomial.iterate_derivative_X_pow_eq_smul] - simp only [smul_comp, pow_comp, X_comp, Algebra.mul_smul_comm, eval_smul, eval_mul, - eval_pow, eval_neg, eval_one, eval_sub, eval_X, smul_eq_mul, ge_iff_le, zero_le_one, - Set.uIcc_of_le] - refine ContinuousOn.mul continuousOn_const (ContinuousOn.mul continuousOn_const ?_) - apply ContinuousOn.pow (ContinuousOn.sub continuousOn_const continuousOn_id) + · exact (Polynomial.continuous _).intervalIntegrable _ _ · have : deriv (deriv^[m] fun y ↦ 1 / (1 - (1 - x * y) * z)) = (Function.eval · (deriv (deriv^[m] fun y ↦ 1 / (1 - (1 - x * y) * z)))) := by ext x @@ -566,24 +453,25 @@ lemma integral_shiftedLegendre_mul_smooth_eq_aux {x z : ℝ} (n m : ℕ) (h : m rw [← Set.uIcc_of_le (by norm_num)] apply special_deriv_div_continuousOn hx hz -lemma integral_legendre_mul_smooth_eq {x z : ℝ} (n : ℕ) (hx : x ∈ Set.Ioo 0 1) (hz : z ∈ Set.Ioo 0 1) : - ∫ (y : ℝ) in (0)..1, eval y (shiftedLegendre n) * (fun y ↦ 1 / (1 - (1 - x * y) * z)) y = +lemma integral_legendre_mul_smooth_eq {x z : ℝ} (n : ℕ) + (hx : x ∈ Set.Ioo 0 1) (hz : z ∈ Set.Ioo 0 1) : + ∫ (y : ℝ) in (0)..1, eval y (aperyShiftedLegendre n) * (fun y ↦ 1 / (1 - (1 - x * y) * z)) y = (- 1) ^ n / n ! * ∫ (y : ℝ) in (0)..1, y ^ n * (1 - y) ^ n * (deriv^[n] fun y ↦ 1 / (1 - (1 - x * y) * z)) y := by - simp only [eval_mul, one_div, eval_C, shiftedLegendre] + simp only [eval_mul, one_div, eval_C, aperyShiftedLegendre_eq_rodrigues] simp_rw [mul_assoc, intervalIntegral.integral_const_mul] rw [← mul_one_div, one_div] nth_rw 4 [mul_comm] rw [mul_assoc] congr obtain h := integral_shiftedLegendre_mul_smooth_eq_aux (n := n) (m := n) (by norm_num) hx hz - simp only [one_div, ge_iff_le, le_refl, tsub_eq_zero_of_le, Function.iterate_zero, id_eq, + simp only [one_div, le_refl, tsub_eq_zero_of_le, Function.iterate_zero, id_eq, eval_mul, eval_pow, eval_X, eval_sub, eval_one] at h rw [h] simp_rw [← mul_assoc] lemma legendre_integral_special {x z : ℝ} (n : ℕ) (hx : x ∈ Set.Ioo 0 1) (hz : z ∈ Set.Ioo 0 1) : - ∫ (y : ℝ) in (0)..1, eval y (shiftedLegendre n) * (1 / (1 - (1 - x * y) * z)) = + ∫ (y : ℝ) in (0)..1, eval y (aperyShiftedLegendre n) * (1 / (1 - (1 - x * y) * z)) = ∫ (y : ℝ) in (0)..1, (x * y * z) ^ n * (1 - y) ^ n / (1 - (1 - x * y) * z) ^ (n + 1) := by rw [integral_legendre_mul_smooth_eq n hx hz, ← intervalIntegral.integral_const_mul, intervalIntegral.integral_of_le (by norm_num), intervalIntegral.integral_of_le (by norm_num), @@ -622,3 +510,5 @@ lemma legendre_integral_special {x z : ℝ} (n : ℕ) (hx : x ∈ Set.Ioo 0 1) ( apply mul_le_of_le_one_left (by linarith) simp only [tsub_le_iff_right, le_add_iff_nonneg_right] nlinarith + +end Polynomial diff --git a/Zeta3Irrational/LinearForm.lean b/Zeta3Irrational/LinearForm.lean index e90d872..4c678c9 100644 --- a/Zeta3Irrational/LinearForm.lean +++ b/Zeta3Irrational/LinearForm.lean @@ -1,6 +1,8 @@ import Zeta3Irrational.Integral import Zeta3Irrational.d +/-! # Integer linear forms for the Apéry integrals -/ + open scoped Nat open BigOperators @@ -17,7 +19,7 @@ lemma J_rr_linear (r : ℕ) : simp only [sub_right_inj] simp_rw [eq_div_iff d_cube_ne_zero, Finset.mul_sum, Finset.sum_mul] use ∑ i ∈ Finset.Icc 1 r, 2 * ↑(d (Finset.Icc 1 r)) ^ 3 / ↑i ^ 3 - simp only [Int.cast_sum, Int.cast_mul, Int.cast_ofNat, Int.cast_pow, Int.cast_natCast] + simp only [Int.cast_sum] apply Finset.sum_congr rfl intro x hx rw [mul_assoc] @@ -33,7 +35,8 @@ lemma J_rr_linear (r : ℕ) : not_false_eq_true, pow_eq_zero_iff, Nat.cast_eq_zero] linarith -lemma Icc_diff_Icc {r s : ℕ} (_ : r > s) (_ : ¬s = 0) : Finset.Icc 1 r \ Finset.Icc 1 s = Finset.Icc (s + 1) r := by +lemma Icc_diff_Icc {r s : ℕ} (_ : r > s) (_ : ¬s = 0) : + Finset.Icc 1 r \ Finset.Icc 1 s = Finset.Icc (s + 1) r := by ext x constructor · intro hx @@ -54,9 +57,9 @@ lemma one_div_sum_eq {r s : ℕ} (h : r > s) : simp_all else simp_rw [← Nat.cast_add] - rw [Icc_diff_Icc h h1, ← Nat.Ico_succ_right, ← Nat.Ico_succ_right, - Finset.sum_Ico_add (f := fun (x : ℕ) => 1 / ((x ^ 2) : ℝ)) (c := s), Nat.succ_eq_add_one, - Nat.succ_eq_add_one, add_comm, show r - s + 1 + s = r + 1 by omega] + rw [Icc_diff_Icc h h1, ← Finset.Ico_add_one_right_eq_Icc, ← Finset.Ico_add_one_right_eq_Icc, + Finset.sum_Ico_add (f := fun (x : ℕ) => 1 / ((x ^ 2) : ℝ)) (c := s), add_comm, + show r - s + 1 + s = r + 1 by omega] · exact Finset.Icc_subset_Icc_right (LT.lt.le (gt_iff_lt.1 h)) lemma J_rs_linear {r s : ℕ} (h : r > s) : ∃ a : ℤ, J r s = a / (d (Finset.Icc 1 r)) ^ 3 := by @@ -76,7 +79,7 @@ lemma J_rs_linear {r s : ℕ} (h : r > s) : ∃ a : ℤ, J r s = a / (d (Finset. · norm_cast rw [d_sq'] apply dvd_d_of_mem - simp_all only [gt_iff_lt, Finset.mem_Icc, Finset.mem_image, ge_iff_le, zero_le, ne_eq, + simp_all only [gt_iff_lt, Finset.mem_Icc, Finset.mem_image, zero_le, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_left_inj₀, exists_eq_right] omega · simp_all only [gt_iff_lt, Finset.mem_Icc, Int.cast_pow, Int.cast_add, Int.cast_natCast, @@ -94,38 +97,44 @@ lemma J_rs_linear {r s : ℕ} (h : r > s) : ∃ a : ℤ, J r s = a / (d (Finset. rw [← Nat.cast_sub (by linarith)] norm_cast; linarith -lemma multi_integral_sum_comm (c : ℕ → ℤ) : ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, +lemma multi_integral_sum_comm {n : ℕ} (c : ℕ → ℤ) : ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, ∑ x_1 ∈ Finset.range (n + 1), ∑ x_2 ∈ Finset.range (n + 1), -(x.1 * x.2).log / (1 - x.1 * x.2) * ↑(c x_1) * x.1 ^ x_1 * ↑(c x_2) * x.2 ^ x_2 - = ∑ x_1 ∈ Finset.range (n + 1), ∑ x_2 ∈ Finset.range (n + 1), ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, + = ∑ x_1 ∈ Finset.range (n + 1), ∑ x_2 ∈ Finset.range (n + 1), + ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, -(x.1 * x.2).log / (1 - x.1 * x.2) * ↑(c x_1) * x.1 ^ x_1 * ↑(c x_2) * x.2 ^ x_2 := by symm calc - _ = ∑ x_1 ∈ Finset.range (n + 1), ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, ∑ x_2 ∈ Finset.range (n + 1), + _ = ∑ x_1 ∈ Finset.range (n + 1), ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, + ∑ x_2 ∈ Finset.range (n + 1), -(x.1 * x.2).log / (1 - x.1 * x.2) * ↑(c x_1) * x.1 ^ x_1 * ↑(c x_2) * x.2 ^ x_2 := by congr! 1 with a _ - rw [← MeasureTheory.integral_finset_sum] + rw [← MeasureTheory.integral_finsetSum] intro i _ have h : (fun (x : ℝ × ℝ) ↦ -Real.log (x.1 * x.2) / (1 - x.1 * x.2) * ↑(c a) * x.1 ^ a * - ↑(c i) * x.2 ^ i) = (fun x ↦ -Real.log (x.1 * x.2) / (1 - x.1 * x.2) * x.1 ^ a * x.2 ^ i * (↑(c i) * ↑(c a))) := by + ↑(c i) * x.2 ^ i) = (fun x ↦ -Real.log (x.1 * x.2) / (1 - x.1 * x.2) * + x.1 ^ a * x.2 ^ i * (↑(c i) * ↑(c a))) := by ext x; ring rw [h] apply MeasureTheory.Integrable.mul_const exact integrableOn_J_rs a i - _ = ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, ∑ x_1 ∈ Finset.range (n + 1), ∑ x_2 ∈ Finset.range (n + 1), + _ = ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, + ∑ x_1 ∈ Finset.range (n + 1), ∑ x_2 ∈ Finset.range (n + 1), -(x.1 * x.2).log / (1 - x.1 * x.2) * ↑(c x_1) * x.1 ^ x_1 * ↑(c x_2) * x.2 ^ x_2 := by - rw [← MeasureTheory.integral_finset_sum] + rw [← MeasureTheory.integral_finsetSum] intro i _ - apply MeasureTheory.integrable_finset_sum + apply MeasureTheory.integrable_finsetSum intro j _ have h : (fun (x : ℝ × ℝ) ↦ -Real.log (x.1 * x.2) / (1 - x.1 * x.2) * ↑(c i) * x.1 ^ i * - ↑(c j) * x.2 ^ j) = (fun x ↦ -Real.log (x.1 * x.2) / (1 - x.1 * x.2) * x.1 ^ i * x.2 ^ j * (↑(c i) * ↑(c j))) := by + ↑(c j) * x.2 ^ j) = (fun x ↦ -Real.log (x.1 * x.2) / (1 - x.1 * x.2) * + x.1 ^ i * x.2 ^ j * (↑(c i) * ↑(c j))) := by ext x; ring rw [h] apply MeasureTheory.Integrable.mul_const exact integrableOn_J_rs i j -lemma multi_integral_mul_const (c d : ℕ) (p q : ℝ): ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, +lemma multi_integral_mul_const (c d : ℕ) (p q : ℝ) : + ∫ (x : ℝ × ℝ) in Set.Ioo 0 1 ×ˢ Set.Ioo 0 1, -(x.1 * x.2).log / (1 - x.1 * x.2) * p * x.1 ^ c * q * x.2 ^ d = p * q * J c d := by simp only [J] symm @@ -135,11 +144,13 @@ lemma multi_integral_mul_const (c d : ℕ) (p q : ℝ): ∫ (x : ℝ × ℝ) in simp only [smul_eq_mul] ring +/-- Integer correction coefficient selected from the proved integral identities. -/ noncomputable def p (r s : ℕ) : ℤ := if h : r > s then (J_rs_linear h).choose else if h : r < s then (J_rs_linear h).choose else -(J_rr_linear r).choose +/-- The zeta coefficient: two on the diagonal and zero off the diagonal. -/ noncomputable def q (r s : ℕ) : ℤ := if r > s then 0 else if r < s then 0 @@ -156,27 +167,27 @@ lemma linear_int_aux : ∃ a b : ℕ → ℕ → ℤ, ∀ r s : ℕ, J r s = use q intro x y if h : x > y then - cases' (J_rs_linear h) with a ha + obtain ⟨a, ha⟩ := J_rs_linear h simp only [p, q] - simp_all only [gt_iff_lt, one_div, dite_eq_ite, ite_true, Int.cast_zero, zero_mul, dite_true, + simp_all only [gt_iff_lt, one_div, ite_true, Int.cast_zero, zero_mul, dite_true, zero_add] rw [(J_rs_linear h).choose_spec] at ha rw [show x.max y = x by exact max_eq_left_iff.2 (LT.lt.le h)] simp_all else if h1 : x < y then - cases' (J_rs_linear h1) with a ha + obtain ⟨a, ha⟩ := J_rs_linear h1 simp only [p, q] obtain h2 := J_symm x y - simp_all only [gt_iff_lt, one_div, dite_eq_ite, ite_true, ite_self, Int.cast_zero, - zero_mul, dite_true, zero_add, not_false_eq_true, dite_false] + simp_all only [gt_iff_lt, one_div, ite_true, ite_self, Int.cast_zero, + zero_mul, dite_true, zero_add, dite_false] rw [(J_rs_linear h1).choose_spec] at ha simp only [not_lt] at h simp_all else have h : x = y := by linarith - cases' (J_rr_linear y) with a ha + obtain ⟨a, ha⟩ := J_rr_linear y simp only [p, q] - simp_all only [gt_iff_lt, lt_self_iff_false, not_false_eq_true, dite_eq_ite, ite_false, + simp_all only [gt_iff_lt, lt_self_iff_false, not_false_eq_true, ite_false, Int.cast_ofNat, not_isEmpty_of_nonempty, tsum_empty, mul_zero, zero_sub, sub_right_inj, dite_false, Int.cast_neg, max_self] rw [(J_rr_linear y).choose_spec, ← Mathlib.Tactic.RingNF.add_neg, ← neg_div] at ha diff --git a/Zeta3Irrational/PrimeCounting.lean b/Zeta3Irrational/PrimeCounting.lean new file mode 100644 index 0000000..07a6c45 --- /dev/null +++ b/Zeta3Irrational/PrimeCounting.lean @@ -0,0 +1,48 @@ +import PrimeNumberTheoremAnd.ZetaFive.Consequences + +/-! +# Prime counting asymptotics from the proved prime number theorem + +The current Mathlib Chebyshev remainder estimate converts the proved theta asymptotic +into the exact all-real prime-counting formula used by the Apéry proof. +-/ + +open Filter Real Asymptotics +open scoped Chebyshev + +namespace AperyPNT + +/-- The prime-counting function is asymptotic to `x / log x`. -/ +theorem primeCounting_asymptotic : + (fun x : ℝ ↦ (Nat.primeCounting ⌊x⌋₊ : ℝ)) ~[atTop] (fun x ↦ x / log x) := by + have h := ZetaFivePNT.chebyshev_asymptotic.div (IsEquivalent.refl (u := Real.log)) + have h' := h.add_isLittleO Chebyshev.integral_theta_div_log_sq_isLittleO + apply h'.congr' ?_ (Filter.EventuallyEq.refl _ _) + filter_upwards [eventually_ge_atTop (2 : ℝ)] with x hx + simp only [Pi.sub_apply, Pi.add_apply, Pi.div_apply, id_eq] + rw [Chebyshev.primeCounting_eq_theta_div_log_add_integral hx] + +/-- The exact prime-counting consequence, with an error tending to zero. -/ +theorem pi_alt : ∃ c : ℝ → ℝ, c =o[atTop] (fun _ ↦ (1 : ℝ)) ∧ + ∀ x : ℝ, Nat.primeCounting ⌊x⌋₊ = (1 + c x) * x / log x := by + refine ⟨fun x ↦ (Nat.primeCounting ⌊x⌋₊ : ℝ) / (x / log x) - 1, ?_, ?_⟩ + · rw [isLittleO_one_iff] + have h := (isEquivalent_iff_tendsto_one ?_).mp primeCounting_asymptotic + · simpa using h.sub (tendsto_const_nhds (x := (1 : ℝ))) + · filter_upwards [eventually_gt_atTop (1 : ℝ)] with x hx + exact div_ne_zero (by positivity) (log_pos hx).ne' + · intro x + by_cases hx : x = 0 + · simp [hx] + by_cases hl : log x = 0 + · have hp : Nat.primeCounting ⌊x⌋₊ = 0 := by + apply Nat.primeCounting_eq_zero_iff.mpr + rcases log_eq_zero.mp hl with h | h | h + · exact (hx h).elim + · simp [h] + · simp [h, Nat.floor_of_nonpos] + simp [hl, hp] + · field_simp + ring + +end AperyPNT diff --git a/Zeta3Irrational/d.lean b/Zeta3Irrational/d.lean index 027628c..343f95f 100644 --- a/Zeta3Irrational/d.lean +++ b/Zeta3Irrational/d.lean @@ -4,32 +4,23 @@ Author: Junqi Liu and Jujian Zhang. -/ import Mathlib.Algebra.GCDMonoid.Finset import Mathlib.Algebra.GCDMonoid.Nat +import Mathlib.Data.Nat.GCD.Prime import Mathlib.Analysis.SpecialFunctions.Log.Base import Mathlib.Data.Nat.Choose.Factorization -import Mathlib.Data.Real.StarOrdered +import Mathlib.Analysis.Real.Sqrt import Mathlib.NumberTheory.PrimeCounting +/-! +# Least common multiples for the Apéry irrationality proof + +We bound the least common multiple of the integers from one to `n` using prime counting. +The natural-number normalization and GCD structures are Mathlib's canonical instances. +-/ + open scoped Nat open BigOperators -instance : NormalizedGCDMonoid ℕ where - normUnit _ := 1 - normUnit_zero := rfl - normUnit_mul := by simp - normUnit_coe_units n := by - rw [Nat.units_eq_one n] - simp - gcd := Nat.gcd - lcm := Nat.lcm - gcd_dvd_left := Nat.gcd_dvd_left - gcd_dvd_right := Nat.gcd_dvd_right - dvd_gcd := Nat.dvd_gcd - gcd_mul_lcm m n := by rw [Nat.gcd_mul_lcm]; rfl - lcm_zero_left := Nat.lcm_zero_left - lcm_zero_right := Nat.lcm_zero_right - normalize_gcd := by simp - normalize_lcm := by simp - +/-- The least common multiple of the natural numbers in the finite set s. -/ def d (s : Finset ℕ) : ℕ := s.lcm id theorem d_insert (s : Finset ℕ) (n : ℕ) : d (insert n s) = Nat.lcm n (d s) := by @@ -57,10 +48,6 @@ theorem d_eq_zero (s : Finset ℕ) (hs : 0 ∈ s) : d s = 0 := by rw [Finset.lcm_eq_zero_iff] simpa -theorem Nat.Prime.dvd_lcm {p} (hp : Nat.Prime p) (a b) (h : p ∣ Nat.lcm a b) : p ∣ a ∨ p ∣ b := by - have := h.trans <| Nat.lcm_dvd_mul a b - rwa [Nat.Prime.dvd_mul hp] at this - theorem Nat.primeFactors_lcm {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : (a.lcm b).primeFactors = a.primeFactors ∪ b.primeFactors := by ext p @@ -69,7 +56,7 @@ theorem Nat.primeFactors_lcm {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : simp only [mem_primeFactorsList', ne_eq] constructor · rintro ⟨hp1, hp2, hp3⟩ - obtain hp4|hp4 := hp1.dvd_lcm a b hp2 + obtain hp4|hp4 := hp1.dvd_or_dvd_of_dvd_lcm hp2 · left; refine ⟨hp1, hp4, ?_⟩ contrapose! hp3 subst hp3 @@ -88,240 +75,17 @@ theorem Nat.primeFactors_lcm {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : erw [lcm_eq_zero_iff] at hp3 refine hp3.elim (fun ha' => absurd ha' ha) id -theorem d_sq (s : Finset ℕ) : (d s)^2 = d (s.image (· ^ 2)) := by +theorem d_sq (s : Finset ℕ) : (d s) ^ 2 = d (s.image (· ^ 2)) := by induction s using Finset.induction_on with | empty => simp [d] - | @insert i s hi ih => - rw [d_insert, Finset.image_insert, d_insert, ← ih] - refine dvd_antisymm ?_ ?_ - · if hi : i = 0 - then - subst hi - simp - else - if hs' : 0 ∈ s - then - rw [d_eq_zero _ hs'] - simp - else - have hds : d s ≠ 0 := d_ne_zero s hs' - have hi' : i^2 ≠ 0 := by simpa using hi - have hds' : (d s)^2 ≠ 0 := by simpa using hds - rw [← Nat.factorizationLCMLeft_mul_factorizationLCMRight, - ← Nat.factorizationLCMLeft_mul_factorizationLCMRight, mul_pow] <;> try assumption - - apply mul_dvd_mul - · delta Nat.factorizationLCMLeft - erw [← Finset.prod_pow] - dsimp only - have eq1 := - calc ∏ x ∈ (i.lcm (d s)).factorization.support, - (if (d s).factorization x ≤ i.factorization x - then x ^ (i.lcm (d s)).factorization x else 1) ^ 2 - _ = ∏ x ∈ (i.primeFactors ∪ (d s).primeFactors), - (if (d s).factorization x ≤ i.factorization x - then x ^ (i.lcm (d s)).factorization x else 1) ^ 2 := by - apply Finset.prod_congr ?_ (fun _ _ => rfl) - rw [Nat.support_factorization, Nat.primeFactors_lcm] <;> assumption - _ = ∏ x ∈ (i.primeFactors ∪ (d s).primeFactors), - if (d s).factorization x ≤ i.factorization x - then (x ^ (i.lcm (d s)).factorization x) ^ 2 else 1 := by - refine Finset.prod_congr rfl fun x _ => ?_ - split_ifs <;> simp - rw [eq1] - have eq2 := calc ((i ^ 2).lcm (d s ^ 2)).factorization.prod fun p n ↦ - if (d s ^ 2).factorization p ≤ (i ^ 2).factorization p then p ^ n else 1 - _ = ∏ i ∈ ((i ^ 2).lcm (d s ^ 2)).factorization.support, _ := rfl - _ = ∏ i ∈ (i.primeFactors ∪ (d s).primeFactors), _ := by - apply Finset.prod_congr ?_ (fun _ _ => rfl) - rw [Nat.support_factorization, Nat.primeFactors_lcm] <;> try assumption - congr 1 <;> - · rw [pow_two, Nat.primeFactors_mul] <;> aesop - - simp_rw [eq2, Nat.factorization_pow] - simp only [Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, gt_iff_lt, Nat.ofNat_pos, - mul_le_mul_left] - apply Finset.prod_dvd_prod_of_dvd - intro p _ - split_ifs - · rw [← pow_mul] - apply pow_dvd_pow - rw [Nat.factorization_lcm, Nat.factorization_lcm] <;> try assumption - - simp only [Finsupp.sup_apply, Nat.factorization_pow, Finsupp.coe_smul, Pi.smul_apply, - smul_eq_mul] - have eq : 2 * i.factorization p ⊔ 2 * (d s).factorization p = - 2 * (i.factorization p ⊔ (d s).factorization p) := by - change Nat.max _ _ = 2 * Nat.max _ _ - rw [mul_max_of_nonneg] - norm_num - rw [eq, mul_comm] - - · exact one_dvd _ - · delta Nat.factorizationLCMRight - erw [← Finset.prod_pow] - dsimp only - have eq1 := - calc ∏ x ∈ (i.lcm (d s)).factorization.support, - (if (d s).factorization x ≤ i.factorization x - then 1 else x ^ (i.lcm (d s)).factorization x) ^ 2 - _ = ∏ x ∈ (i.primeFactors ∪ (d s).primeFactors), - (if (d s).factorization x ≤ i.factorization x - then 1 else x ^ (i.lcm (d s)).factorization x) ^ 2 := by - apply Finset.prod_congr ?_ (fun _ _ => rfl) - rw [Nat.support_factorization, Nat.primeFactors_lcm] <;> assumption - _ = ∏ x ∈ (i.primeFactors ∪ (d s).primeFactors), - if (d s).factorization x ≤ i.factorization x - then 1 else (x ^ (i.lcm (d s)).factorization x) ^ 2 := by - refine Finset.prod_congr rfl fun x _ => ?_ - split_ifs <;> simp - rw [eq1] - have eq2 := calc ((i ^ 2).lcm (d s ^ 2)).factorization.prod fun p n ↦ - if (d s ^ 2).factorization p ≤ (i ^ 2).factorization p then 1 else p ^ n - _ = ∏ i ∈ ((i ^ 2).lcm (d s ^ 2)).factorization.support, _ := rfl - _ = ∏ i ∈ (i.primeFactors ∪ (d s).primeFactors), _ := by - apply Finset.prod_congr ?_ (fun _ _ => rfl) - rw [Nat.support_factorization, Nat.primeFactors_lcm] <;> try assumption - congr 1 <;> - · rw [pow_two, Nat.primeFactors_mul] <;> aesop - simp_rw [eq2, Nat.factorization_pow] - simp only [Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, gt_iff_lt, Nat.ofNat_pos, - mul_le_mul_left] - apply Finset.prod_dvd_prod_of_dvd - intro p _ - split_ifs - · exact one_dvd _ - · rw [← pow_mul] - apply pow_dvd_pow - rw [Nat.factorization_lcm, Nat.factorization_lcm] <;> try assumption + | @insert i s _ ih => + rw [d_insert, Finset.image_insert, d_insert, ← ih, Nat.pow_lcm_pow] - simp only [Finsupp.sup_apply, Nat.factorization_pow, Finsupp.coe_smul, Pi.smul_apply, - smul_eq_mul] - have eq : 2 * i.factorization p ⊔ 2 * (d s).factorization p = - 2 * (i.factorization p ⊔ (d s).factorization p) := by - change Nat.max _ _ = 2 * Nat.max _ _ - rw [mul_max_of_nonneg] - norm_num - rw [eq, mul_comm] - - · rw [Nat.lcm_dvd_iff] - exact ⟨pow_dvd_pow_of_dvd (Nat.dvd_lcm_left _ _) 2, - pow_dvd_pow_of_dvd (Nat.dvd_lcm_right _ _) 2⟩ - -theorem d_cube (s : Finset ℕ) : (d s)^3 = d (s.image (· ^ 3)) := by +theorem d_cube (s : Finset ℕ) : (d s) ^ 3 = d (s.image (· ^ 3)) := by induction s using Finset.induction_on with | empty => simp [d] - | @insert i s hi ih => - rw [d_insert, Finset.image_insert, d_insert, ← ih] - refine dvd_antisymm ?_ ?_ - · if hi : i = 0 - then - subst hi - simp - else - if hs' : 0 ∈ s - then - rw [d_eq_zero _ hs'] - simp - else - have hds : d s ≠ 0 := d_ne_zero s hs' - have hi' : i^3 ≠ 0 := by simpa using hi - have hds' : (d s)^3 ≠ 0 := by simpa using hds - rw [← Nat.factorizationLCMLeft_mul_factorizationLCMRight, - ← Nat.factorizationLCMLeft_mul_factorizationLCMRight, mul_pow] <;> try assumption - - apply mul_dvd_mul - · delta Nat.factorizationLCMLeft - erw [← Finset.prod_pow] - dsimp only - have eq1 := - calc ∏ x ∈ (i.lcm (d s)).factorization.support, - (if (d s).factorization x ≤ i.factorization x - then x ^ (i.lcm (d s)).factorization x else 1) ^ 3 - _ = ∏ x ∈ (i.primeFactors ∪ (d s).primeFactors), - (if (d s).factorization x ≤ i.factorization x - then x ^ (i.lcm (d s)).factorization x else 1) ^ 3 := by - apply Finset.prod_congr ?_ (fun _ _ => rfl) - rw [Nat.support_factorization, Nat.primeFactors_lcm] <;> assumption - _ = ∏ x ∈ (i.primeFactors ∪ (d s).primeFactors), - if (d s).factorization x ≤ i.factorization x - then (x ^ (i.lcm (d s)).factorization x) ^ 3 else 1 := by - refine Finset.prod_congr rfl fun x _ => ?_ - split_ifs <;> simp - rw [eq1] - have eq2 := calc ((i ^ 3).lcm (d s ^ 3)).factorization.prod fun p n ↦ - if (d s ^ 3).factorization p ≤ (i ^ 3).factorization p then p ^ n else 1 - _ = ∏ i ∈ ((i ^ 3).lcm (d s ^ 3)).factorization.support, _ := rfl - _ = ∏ i ∈ (i.primeFactors ∪ (d s).primeFactors), _ := by - apply Finset.prod_congr ?_ (fun _ _ => rfl) - rw [Nat.support_factorization, Nat.primeFactors_lcm] <;> try assumption - congr 1 <;> - · rw [show 3 = 2 + 1 by omega, pow_add, pow_two, pow_one, Nat.primeFactors_mul, - Nat.primeFactors_mul] <;> aesop - - simp_rw [eq2, Nat.factorization_pow] - simp only [Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, gt_iff_lt, Nat.ofNat_pos, - mul_le_mul_left] - apply Finset.prod_dvd_prod_of_dvd - intro p _ - split_ifs - · rw [← pow_mul] - apply pow_dvd_pow - rw [Nat.factorization_lcm, Nat.factorization_lcm] <;> try assumption - - simp only [Finsupp.sup_apply, Nat.factorization_pow, Finsupp.coe_smul, Pi.smul_apply, - smul_eq_mul] - have eq : 3 * i.factorization p ⊔ 3 * (d s).factorization p = - 3 * (i.factorization p ⊔ (d s).factorization p) := by - change Nat.max _ _ = 3 * Nat.max _ _ - rw [mul_max_of_nonneg] - norm_num - rw [eq, mul_comm] - · exact one_dvd _ - - · delta Nat.factorizationLCMRight - erw [← Finset.prod_pow] - simp only [Nat.support_factorization, ite_pow, one_pow, Nat.factorization_pow, - Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, gt_iff_lt, Nat.ofNat_pos, mul_le_mul_left] - have eq1 := - calc ∏ x ∈ (i.lcm (d s)).primeFactors, - if (d s).factorization x ≤ i.factorization x - then 1 else (x ^ (i.lcm (d s)).factorization x) ^ 3 - _ = ∏ x ∈ (i.primeFactors ∪ (d s).primeFactors), - if (d s).factorization x ≤ i.factorization x - then 1 else (x ^ (i.lcm (d s)).factorization x) ^ 3 := by - apply Finset.prod_congr ?_ fun _ _ => rfl - rw [Nat.primeFactors_lcm] <;> assumption - rw [eq1] - have eq2 := calc ((i ^ 3).lcm (d s ^ 3)).factorization.prod fun p n ↦ - if (d s).factorization p ≤ i.factorization p then 1 else p ^ n - _ = ∏ i ∈ ((i ^ 3).lcm (d s ^ 3)).factorization.support, _ := rfl - _ = ∏ i ∈ (i.primeFactors ∪ (d s).primeFactors), _ := by - apply Finset.prod_congr ?_ fun _ _ => rfl - rw [Nat.support_factorization, Nat.primeFactors_lcm] <;> try assumption - congr 1 <;> - · rw [show 3 = 2 + 1 by omega, pow_add, pow_two, pow_one, Nat.primeFactors_mul, - Nat.primeFactors_mul] <;> aesop - rw [eq2] - apply Finset.prod_dvd_prod_of_dvd - intro p _ - simp only - split_ifs - · simp - · rw [← pow_mul] - apply pow_dvd_pow - rw [Nat.factorization_lcm, Nat.factorization_lcm] <;> try assumption - simp only [Finsupp.sup_apply, Nat.factorization_pow, Finsupp.coe_smul, Pi.smul_apply, - smul_eq_mul] - have eq : 3 * i.factorization p ⊔ 3 * (d s).factorization p = - 3 * (i.factorization p ⊔ (d s).factorization p) := by - change Nat.max _ _ = 3 * Nat.max _ _ - rw [mul_max_of_nonneg] - norm_num - rw [eq, mul_comm] - · rw [Nat.lcm_dvd_iff] - exact ⟨pow_dvd_pow_of_dvd (Nat.dvd_lcm_left _ _) 3, - pow_dvd_pow_of_dvd (Nat.dvd_lcm_right _ _) 3⟩ + | @insert i s _ ih => + rw [d_insert, Finset.image_insert, d_insert, ← ih, Nat.pow_lcm_pow] theorem d_sq' (n : ℕ) : d (Finset.Icc 1 n)^2 = d (Finset.Icc 1 n |>.image (· ^ 2)) := d_sq _ @@ -339,12 +103,6 @@ theorem lcm_factorization (m n p : ℕ) (hm : m ≠ 0) (hn : n ≠ 0) : rw [Nat.factorization_lcm hm hn] aesop --- lemma lcm_eq_prod (m n : ℕ) : m.lcm n = --- ∏ p ∈ (max m n).primesBelow, p ^ (max (m.factorization p) (n.factorization p)) := by - --- sorry - - theorem d_factorization (s : Finset ℕ) (hs : s.Nonempty) (p : ℕ) (hs₁ : 0 ∉ s) : (d s).factorization p = (s.image fun i => i.factorization p).max' (by aesop) := by @@ -356,15 +114,11 @@ theorem d_factorization (s : Finset ℕ) (hs : s.Nonempty) (p : ℕ) (hs₁ : 0 then simp only [Finset.image_insert] rw [Finset.max'_insert (H := by aesop)] - rw [max_comm] - congr 1 - rw [ih hs] - aesop + rw [ih hs (by aesop)] else simp only [Finset.not_nonempty_iff_eq_empty] at hs subst hs - simp only [d_empty, Nat.factorization_one, Finsupp.coe_zero, Pi.zero_apply, zero_le, - max_eq_left, insert_emptyc_eq, Finset.image_singleton, Finset.max'_singleton] + simp [d_empty] · aesop · apply d_ne_zero aesop @@ -431,14 +185,16 @@ theorem d_factorization_eq_div_log' (n p : ℕ) (hp : Nat.Prime p) : · by_contra! h rw [Finset.max'_le_iff] at h set y := (Finset.image (fun i ↦ i.factorization p) (Finset.Icc 1 (n + 1))).max' (by aesop) - have hy : (y : ℝ) ∈ (Finset.image (fun i ↦ (i.factorization p : ℝ)) (Finset.Icc 1 (n + 1))) := by + have hy : (y : ℝ) ∈ + (Finset.image (fun i ↦ (i.factorization p : ℝ)) (Finset.Icc 1 (n + 1))) := by simp only [Finset.mem_image, Finset.mem_Icc, Nat.cast_inj] simp_rw [← Finset.mem_Icc] rw [← Finset.mem_image] exact Finset.max'_mem _ _ specialize h (y : ℝ) hy rw [le_sub_iff_add_le, Real.le_logb_iff_rpow_le] at h - · have h2 : y + 1 ∉ (Finset.image (fun i ↦ i.factorization p) (Finset.Icc 1 (n + 1))) := by + · have h2 : y + 1 ∉ + (Finset.image (fun i ↦ i.factorization p) (Finset.Icc 1 (n + 1))) := by by_contra! hy1 suffices y + 1 ≤ y by linarith exact Finset.le_max' _ _ hy1 @@ -450,8 +206,8 @@ theorem d_factorization_eq_div_log' (n p : ℕ) (hp : Nat.Prime p) : exact Nat.Prime.one_lt hp · norm_cast omega - · aesop · aesop + · simp · apply Real.logb_nonneg · norm_cast exact Nat.Prime.one_lt hp @@ -464,31 +220,20 @@ theorem d_factorization_eq_div_log (n p : ℕ) (hp : Nat.Prime p) : cases n · simp only [zero_lt_one, Finset.Icc_eq_empty_of_lt, d_empty, Nat.factorization_one, Finsupp.coe_zero, Pi.zero_apply, CharP.cast_eq_zero, Real.log_zero, zero_div, Nat.floor_zero] - · rw [d_factorization_eq_div_log' (hp := hp)] simp --- lemma d_eq_prod (s : Finset ℕ) (hs : s.Nonempty) : --- d s = --- ∏ p ∈ Nat.primesBelow (s.max' hs), --- p ^ (s.image fun i => i.factorization p).max' (by aesop) := by --- induction s using Finset.induction_on with --- | empty => simp only [Finset.not_nonempty_empty] at hs --- | @insert m s hm ih => --- sorry - theorem d_eq_prod_pow' (n : ℕ) : d (Finset.Icc 1 (n + 1)) = ∏ p ∈ (((n + 1) + 1).primesBelow), p ^ ((Finset.Icc 1 (n + 1)).image (fun i => i.factorization p)).max' (by aesop) := by - rw [← Nat.factorization_prod_pow_eq_self (n := d (Finset.Icc 1 (n + 1)))] + rw [← Nat.prod_factorization_pow_eq_self (n := d (Finset.Icc 1 (n + 1)))] · simp only [Finsupp.prod, Nat.support_factorization] rw [d_primeFactors _ (by aesop)] refine Finset.prod_congr ?_ ?_ · ext p - constructor <;> intro hp <;> simp only at hp ⊢ + constructor <;> intro hp · rw [Finset.mem_sup] at hp - obtain ⟨m, H, h⟩ := hp simp only [Finset.mem_Icc] at H rw [Nat.mem_primesBelow] @@ -541,41 +286,39 @@ theorem d_le_pow_counting (n : ℕ) : d (Finset.Icc 1 n) ≤ n ^ (n.primeCountin calc _ ≤ ∏ _ ∈ ((n + 1).primesBelow), n := by apply Finset.prod_le_prod - · intro p _ - simp only [zero_le] - · intro p hp - rw [Nat.mem_primesBelow] at hp - have h2 : 1 ≤ p := by - by_contra! h - have : p = 0 := by omega - aesop - suffices p ^ (⌊(Real.log (n : ℝ)) / (Real.log (p : ℝ))⌋₊ : ℝ) ≤ (n : ℝ) by norm_cast at this - trans p ^ ((Real.log (n : ℝ)) / (Real.log (p : ℝ))) - · apply Real.rpow_le_rpow_of_exponent_le (by norm_cast) - · apply Nat.floor_le (α := ℝ) - if h2 : n = 1 ∨ p = 1 then - rcases h2 with (rfl | rfl) <;> simp - else - rcases (not_or.1 h2) with ⟨_, h2⟩ - have h1 : 1 < n := by omega - have h2 : 1 < p := by omega - suffices 0 < Real.log (n : ℝ) / Real.log (p : ℝ) by linarith - apply div_pos <;> - exact Real.log_pos (by norm_cast) - · nth_rewrite 1 [← Real.exp_log (x := (p : ℝ)) (by norm_cast), ← Real.exp_one_rpow, - ← Real.rpow_mul (by exact Real.exp_nonneg 1), mul_div, mul_comm, ← mul_div] - if hp : p = 1 then - rw [hp]; simp only [Nat.cast_one, Real.log_one, div_zero, mul_zero, Real.rpow_zero, - Nat.one_le_cast, h1] + intro p hp + rw [Nat.mem_primesBelow] at hp + have h2 : 1 ≤ p := by + by_contra! h + have : p = 0 := by omega + aesop + suffices p ^ (⌊(Real.log (n : ℝ)) / (Real.log (p : ℝ))⌋₊ : ℝ) ≤ (n : ℝ) by norm_cast at this + trans p ^ ((Real.log (n : ℝ)) / (Real.log (p : ℝ))) + · apply Real.rpow_le_rpow_of_exponent_le (by norm_cast) + · apply Nat.floor_le (R := ℝ) + if h2 : n = 1 ∨ p = 1 then + rcases h2 with (rfl | rfl) <;> simp else - rw [div_self, mul_one, Real.exp_one_rpow, Real.exp_log (by norm_cast)] - rw [Real.log_ne_zero] - norm_cast - simp only [not_false_eq_true, and_true] - omega + rcases (not_or.1 h2) with ⟨_, h2⟩ + have h1 : 1 < n := by omega + have h2 : 1 < p := by omega + suffices 0 < Real.log (n : ℝ) / Real.log (p : ℝ) by linarith + apply div_pos <;> + exact Real.log_pos (by norm_cast) + · nth_rewrite 1 [← Real.exp_log (x := (p : ℝ)) (by norm_cast), ← Real.exp_one_rpow, + ← Real.rpow_mul (by exact Real.exp_nonneg 1), mul_div, mul_comm, ← mul_div] + if hp : p = 1 then + rw [hp]; simp only [Nat.cast_one, Real.log_one, div_zero, mul_zero, Real.rpow_zero, + Nat.one_le_cast, h1] + else + rw [div_self, mul_one, Real.exp_one_rpow, Real.exp_log (by norm_cast)] + rw [Real.log_ne_zero] + norm_cast + simp only [not_false_eq_true, and_true] + omega _ ≤ n ^ (n.primeCounting) := by rw [Finset.prod_const] - suffices ((n + 1).primesBelow).card = n.primeCounting by apply Nat.pow_le_pow_right <;> linarith + suffices ((n + 1).primesBelow).card = n.primeCounting by + apply Nat.pow_le_pow_right <;> linarith rw [Nat.primeCounting, ← Nat.primesBelow_card_eq_primeCounting'] -#min_imports diff --git a/lakefile.lean b/lakefile.lean index 6276b4a..38f6ff4 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -11,7 +11,10 @@ package «Zeta3Irrational» where @[default_target] lean_lib «Zeta3Irrational» where - -- add any library configuration options here + roots := #[`Zeta3Irrational] + globs := #[`Zeta3Irrational, `Zeta3Irrational.Basic, `Zeta3Irrational.Bound, + `Zeta3Irrational.Integral, `Zeta3Irrational.LegendrePoly, `Zeta3Irrational.LinearForm, + `Zeta3Irrational.d, `Zeta3Irrational.Equality, `Zeta3Irrational.PrimeCounting] require «PrimeNumberTheoremAnd» from git "https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git" @ "main" diff --git a/lean-toolchain b/lean-toolchain index b2153cd..ba8ebf2 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.18.0 +leanprover/lean4:v4.34.1