New subproject: CH2

Stream: PrimeNumberTheorem+

[Terence Tao]

Launching a further sub-project, this time formalizing (a portion of) the recent preprint of Chirre and Helfgott which estimates sums of non-negative arithmetic functions, and in particular the Chebyshev function $\psi(x) = \sum_{n \leq x} \Lambda(n)$, giving bounds of the form $|\psi(x) - x| \leq \varepsilon x$ for $x \geq x_0$ using zero-free regions of the Riemann hypothesis as input. This can be used to largely replace the earlier results of Buthe that are used in FKS/BKLNW.

An initial blueprint can be found here. The methods are Fourier analytic in nature, and in fact have significant overlap with the proof of the Weak PNT using the Wiener-Ikehara method that is already in the repository. I am still digesting the main part of the paper, but I have some initial tasks PNT#879 PNT#880 PNT#881 PNT#882 PNT#883 which should be relatively straightforward (the first two, for instance, are analogues of lemmas that were proven in Weiner.lean). Basically, this corresponds to Section 2 of the Chirre-Helfgott paper, and lets one upper or lower bound sums of non-negative arithmetic functions in terms of integrals involving certain Fourier-analytic majorants and minorants. It turns out that the optimal such majorants and minorants are known, and the next step is to describe them and establish their basic properties; this is Section 4 of the paper, which will be formalized next.

[Pietro Monticone]

Aristotle disproved S_eq_I as follows:

theorem S_eq_I (a : ℕ → ℝ) (s x T : ℝ) (hs : s ≠ 1) (hT : 0 < T)
    : -- may need a summability hypothesis on a
    let lambda := (2 * π * (s - 1)) / T
    S a s x =
      (x ^ (-s):ℝ) * ∑' n, a n * (x / (n ^ s : ℝ)) * I' lambda ((T / (2 * π)) * log (n / x)) := by
      -- Wait, there's a mistake. We can actually prove the opposite.
      negate_state;
      -- Proof starts here:
      -- Choose $a$ to be the constant sequence $1$, $s = 0$, $x = 2$, and $T = 1$.
      use fun _ => 1, 0, 2, 1
      simp [CH2.S, CH2.I'] at *;
      rw [ Summable.tsum_eq_zero_add ] ; norm_num [ Real.pi_ne_zero ];
      · rw [ tsum_eq_sum ] <;> norm_num [ Real.pi_ne_zero ];
        any_goals exact Finset.range 2;
        · norm_num [ Finset.sum_range_succ, Real.pi_ne_zero ];
          split_ifs <;> linarith [ Real.exp_pos ( 2 * Real.pi * ( Real.pi⁻¹ * ( 1 / 2 ) * Real.log ( 1 / 2 ) ) ) ];
        · exact fun n hn => mul_pos ( by positivity ) ( mul_pos ( by positivity ) ( Real.log_pos ( by rw [ lt_div_iff₀ ] <;> norm_cast ; linarith [ Finset.mem_range.not.mp hn ] ) ) );
      · field_simp;
        refine' summable_of_ne_finset_zero _;
        exacts [ Finset.range 3, fun b hb => if_neg <| not_le_of_gt <| Real.log_pos <| by rw [ lt_div_iff₀ ] <;> norm_cast ; linarith [ Finset.mem_range.not.mp hb ] ]

[Harald Helfgott]

@Pietro Monticone, can you tell us which subtask this is?

[David Michael Roberts]

Is it here? https://alexkontorovich.github.io/PrimeNumberTheoremAnd/docs/PrimeNumberTheoremAnd/CH2.html#CH2.S_eq_I with label CH2 Equation (2.10)

@Harald Helfgott
Blueprint: https://alexkontorovich.github.io/PrimeNumberTheoremAnd/blueprint/primary-chapter.html#ch2-2-10 in section "9.6 Chirre-Helfgott’s estimates for sums of nonnegative arithmetic functions"

so.... this? https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/issues/881

[Harald Helfgott]

Is it not yet another case where the convention set at the beginning of the paper (sums on $n$ go from $n=1$ to $\infty$ unless otherwise noted) is forgotten?

[David Michael Roberts]

I'm not a Lean-speaker, but the syntax ∑' (n : ℕ) makes that look like it's a sum starting from 0, yes.

[Pietro Monticone]

Aristotle disproved cor_1_3_b as follows:

noncomputable section AristotleLemmas
/-
Disproof of Corollary 1.3 part b.
-/
theorem cor_1_3_b_disproof : ¬ (∀ x : ℝ, 1 ≤ x → ∃ E : ℝ, ∑ n ∈ Finset.Iic (⌊x⌋₊), Λ n / (n:ℝ) ^ (-(Real.log x - Real.eulerMascheroniConstant)) = Real.log x - Real.eulerMascheroniConstant + E ∧ |E| ≤ Real.pi * Real.sqrt 3 * 10 ^ 12 + 113.67 / x) := by
  push_neg;
  use Real.exp 100;
  refine' ⟨ by norm_num, fun x hx => _ ⟩;
  -- We'll use that $2^{99.4} > 10^{29}$ to show that the term for $n=2$ is much larger than the right-hand side.
  have h_term2 : (Λ 2) / (2 : ℝ) ^ (-(Real.log (Real.exp 100) - Real.eulerMascheroniConstant)) > 10 ^ 29 := by
    norm_num [ Real.rpow_def_of_pos, Real.log_exp ] at *;
    rw [ lt_div_iff₀ ( Real.exp_pos _ ) ];
    refine' lt_of_le_of_lt ( mul_le_mul_of_nonneg_left ( Real.exp_le_exp.mpr <| mul_le_mul_of_nonneg_left ( show Real.eulerMascheroniConstant - 100 ≤ -99 by
                                                                                                              have h_gamma_le_one : ∀ n : ℕ, n ≥ 1 → (∑ k ∈ Finset.range n, (1 / (k + 1) : ℝ)) - Real.log n ≤ 1 := by
                                                                                                                intro n hn; induction' hn with n hn ih <;> norm_num [ Finset.sum_range_succ ] at *;
                                                                                                                field_simp;
                                                                                                                have := Real.log_le_sub_one_of_pos ( by positivity : 0 < ( n : ℝ ) / ( n + 1 ) );
                                                                                                                rw [ Real.log_div ] at this <;> norm_num at * <;> nlinarith [ mul_div_cancel₀ ( n : ℝ ) ( by positivity : ( n : ℝ ) + 1 ≠ 0 ) ];
                                                                                                              -- By definition of Euler-Mascheroni constant, we know that $\gamma = \lim_{n \to \infty} (\sum_{k=1}^n \frac{1}{k} - \log n)$.
                                                                                                              have h_gamma_def : Filter.Tendsto (fun n : ℕ => (∑ k ∈ Finset.range n, (1 / (k + 1) : ℝ)) - Real.log n) Filter.atTop (nhds Real.eulerMascheroniConstant) := by
                                                                                                                convert Real.tendsto_harmonic_sub_log using 1;
                                                                                                                norm_num [ harmonic ];
                                                                                                              exact le_of_tendsto_of_tendsto h_gamma_def tendsto_const_nhds ( Filter.eventually_atTop.mpr ⟨ 1, fun n hn => h_gamma_le_one n hn ⟩ ) |> fun h => by linarith; ) <| Real.log_nonneg <| by norm_num ) <| by norm_num ) _ ; norm_num [ Real.exp_neg, Real.exp_mul, Real.exp_log ];
    norm_num [ ArithmeticFunction.vonMangoldt ];
    rw [ if_pos ];
    · exact Real.log_two_gt_d9.trans_le' <| by norm_num;
    · native_decide +revert;
  -- Since $2^{99.4} > 10^{29}$, we have $\sum_{n=1}^{\lfloor e^{100} \rfloor} \frac{\Lambda(n)}{n^{-(\log(e^{100}) - \gamma)}} \geq \frac{\Lambda(2)}{2^{-(\log(e^{100}) - \gamma)}}$.
  have h_sum_ge_term2 : ∑ n ∈ Finset.Iic ⌊Real.exp 100⌋₊, (Λ n) / (n : ℝ) ^ (-(Real.log (Real.exp 100) - Real.eulerMascheroniConstant)) ≥ (Λ 2) / (2 : ℝ) ^ (-(Real.log (Real.exp 100) - Real.eulerMascheroniConstant)) := by
    refine' le_trans _ ( Finset.single_le_sum ( fun n _ => div_nonneg ( show 0 ≤ Λ n from _ ) ( Real.rpow_nonneg ( Nat.cast_nonneg n ) _ ) ) ( show 2 ∈ Finset.Iic ⌊rexp 100⌋₊ from _ ) ) <;> norm_num;
    exact Nat.le_floor <| by norm_num; linarith [ Real.add_one_le_exp 100 ] ;
  -- Since $|x| \geq 10^{29} - 100 + \gamma$, and $\pi \sqrt{3} \cdot 10^{12} + 113.67 / e^{100}$ is much smaller than $10^{29}$, we have $|x| > \pi \sqrt{3} \cdot 10^{12} + 113.67 / e^{100}$.
  have h_abs_x : |x| ≥ 10 ^ 29 - 100 + Real.eulerMascheroniConstant := by
    cases abs_cases x <;> linarith [ Real.log_exp 100 ];
  refine' lt_of_lt_of_le ( add_lt_add_left ( div_lt_self ( by norm_num ) ( by norm_num ) ) _ ) _;
  have h_pi_approx : Real.pi < 3.15 := by
    exact?;
  have h_euler_approx : Real.eulerMascheroniConstant > 0.5 := by
    have h_gamma_approx : Real.eulerMascheroniConstant > 1 / 2 := by
      exact?;
    exact lt_of_le_of_lt ( by norm_num ) h_gamma_approx;
  norm_num at * ; nlinarith [ Real.sqrt_nonneg 3, Real.sq_sqrt zero_le_three ]

end AristotleLemmas

/-
**Corollary 1.3, part b**

For $x \geq 1$,
$$ \sum_{n \leq x} \frac{\Lambda(n)}{n^{-(\log x - \gamma)}} = \log x - \gamma + O^*(\pi \cdot \sqrt{3} \cdot 10^{12} + 113.67 / x).$$
-/
theorem cor_1_3_b (x : ℝ) (hx : 1 ≤ x) : ∃ E,
    ∑ n ∈ Finset.Iic (⌊x⌋₊), Λ n / (n:ℝ) ^ (-(log x - eulerMascheroniConstant)) =
      log x - eulerMascheroniConstant + E ∧ |E| ≤ π * sqrt 3 * 10 ^ 12 + 113.67 / x := by
        -- Wait, there's a mistake. We can actually prove the opposite.
        negate_state;
        -- Proof starts here:
        -- Apply the disproof of the corollary to obtain the existence of such an x.
        apply Classical.byContradiction
        intro h_contra
        push_neg at h_contra
        exact cor_1_3_b_disproof h_contra

[Terence Tao]

OK, there were some typos. (I had gotten lazy and had cut and pasted text directly from the PDF to get Copilot to formalize, but the cut and paste flattened some subscripts etc. and managed to confuse the AI. More recently I have started cutting and pasting from the LaTeX source of papers, which is more reliable.) Fixing it now.

And yes, I have consistently misformalized sums over the positive integers to be sums over the natural numbers. Will fix that also.

[Pietro Monticone]

Ok, great. Thanks!

[Pietro Monticone]

Aristotle disproved cor_1_2_b as follows:

theorem cor_1_2_b {T x : ℝ} (hT : 1e7 ≤ T) (RH : riemannZeta.RH_up_to T) (hx : max T 1e9 < x) :
    ∑ n ∈ Finset.Iic (⌊x⌋₊), Λ n / (n:ℝ) ^ (-(log x - eulerMascheroniConstant)) ≤
      π * sqrt T⁻¹ + (1 / (2 * π)) * log (T / (2 * π)) ^ 2 - (1 / (6 * π)) * log (T / (2 * π)) / x := by
    -- Wait, there's a mistake. We can actually prove the opposite.
    negate_state;
    -- Proof starts here:
    refine' ⟨ 10^7, 10^9 + 2, _, _, _, _ ⟩ <;> norm_num;
    · -- Apply the lemma that states if the Riemann hypothesis holds up to a certain height, then it holds up to any smaller height.
      apply RH_up_to_mono (by norm_num) Platt_theorem;
    · refine' lt_of_lt_of_le _ ( Finset.single_le_sum ( fun x _ => _ ) ( Finset.mem_Iic.mpr ( show 2 ≤ 1000000002 by norm_num ) ) );
      · convert lhs_bound_val_n2.trans_le' _ using 1;
        · grind;
        · convert rhs_bound_val.le.trans _ using 1 ; norm_num [ Real.pi_pos.ne' ];
          norm_num +zetaDelta at *;
      · exact div_nonneg ( by exact? ) ( Real.rpow_nonneg ( Nat.cast_nonneg _ ) _ )

[Terence Tao]

This was a typo: the denominator on the LHS should have been just n not (n:ℝ) ^ (-(log x - eulerMascheroniConstant)). This should be fixed in the latest version of the repo.

[Pietro Monticone]

Aristotle indirectly disproved prop_2_4_minus as follows:

theorem F.minus_minorizes_I (lambda y : ℝ) (hlam : lambda ≠ 0) :
    F lambda (-1) y ≤ I' lambda y := by
      have := @CH2.prop_2_4_minus;
      contrapose! this;
      refine' ⟨ fun _ => 0, _, 2, 2, _, _, _, _ ⟩ <;> norm_num;
      · exact summable_zero;
      · refine' ⟨ fun _ => 0, _, _, _ ⟩ <;> norm_num [ Set.EqOn ];
        · exact continuousOn_const;
        · intro x hx; rw [ sub_eq_zero ] ; norm_num [ Complex.ext_iff ] ;
          convert CH2.S_eq_I ( fun _ => 1 ) 2 1 1 ; norm_num;
          unfold CH2.S; norm_num [ CH2.I' ] ;
          rw [ Summable.tsum_eq_zero_add ] <;> norm_num;
          · rw [ ← Equiv.tsum_eq ( Equiv.pnatEquivNat ) ] ; norm_num [ Real.pi_ne_zero ];
            norm_num [ PNat.natPred, mul_assoc, mul_comm, mul_left_comm, Real.pi_ne_zero ];
            rw [ tsum_congr fun n => if_pos <| Real.log_nonneg <| mod_cast PNat.one_le _ ] ; ring ; norm_num [ Real.exp_neg, Real.exp_log ];
            refine' iff_of_false ( by rintro ⟨ h₁, h₂ ⟩ ; linarith ) ( ne_of_gt <| _ );
            field_simp;
            fapply Summable.tsum_lt_tsum;
            exacts [ 1 + 1, fun n => one_div_le_one_div_of_le ( by positivity ) ( mod_cast Nat.pow_le_pow_right n.pos ( by decide ) ), by norm_num, by exact Summable.subtype ( Real.summable_one_div_nat_pow.2 ( by decide ) ) _, by exact Summable.subtype ( Real.summable_one_div_nat_pow.2 ( by decide ) ) _ ];
          · exact Summable.of_nonneg_of_le ( fun n => by positivity ) ( fun n => by aesop ) ( Real.summable_one_div_nat_pow.2 one_lt_two );
        · refine' ⟨ fun x => if x = 0 then 1 else 0, _, _, _, _, _ ⟩ <;> norm_num [ CH2.S ];
          · exact Measurable.ite ( MeasurableSet.singleton 0 ) measurable_const measurable_const;
          · exact MeasureTheory.integrable_indicator_iff ( MeasurableSingletonClass.measurableSet_singleton 0 ) |>.2 ( by norm_num );
          · exact fun x hx => by rintro rfl; exact absurd ( hx ( by norm_num ) ) ( by norm_num ) ;
          · refine' ⟨ 0, fun y hy => _ ⟩ ; norm_num [ Real.fourierIntegral ];
            rw [ VectorFourier.fourierIntegral ];
            rw [ MeasureTheory.integral_eq_zero_of_ae ] ; filter_upwards [ MeasureTheory.measure_eq_zero_iff_ae_notMem.1 ( MeasureTheory.measure_singleton 0 ) ] with x hx ; aesop;
          · refine' ⟨ _, 1, _, 2, _, _ ⟩ <;> norm_num [ Real.pi_pos ];
            intro y s hs; rw [ show ( fun x : ℝ => if x = 0 then ( 1 : ℂ ) else 0 ) = ( fun x : ℝ => if x = 0 then ( 1 : ℂ ) else 0 ) from rfl ] ; rw [ show ( 𝓕 ( fun x : ℝ => if x = 0 then ( 1 : ℂ ) else 0 ) ) y = ( 0 : ℂ ) from ?_ ] ; norm_num [ CH2.I' ] ;
            · split_ifs <;> positivity;
            · rw [ Real.fourierIntegral ];
              norm_num [ VectorFourier.fourierIntegral ];
              rw [ MeasureTheory.integral_eq_zero_of_ae ] ; filter_upwards [ MeasureTheory.measure_eq_zero_iff_ae_notMem.mp ( MeasureTheory.measure_singleton 0 ) ] with x hx ; aesop

[Pietro Monticone]

Aristotle disproved S_eq_I, fixed it by adding (hx : 0 < x) and proved S_eq_I_corrected as follows:

theorem S_eq_I (a : ℕ → ℝ) (s x T : ℝ) (hs : s ≠ 1) (hT : 0 < T)
    : -- may need a summability hypothesis on a
    let lambda := (2 * π * (s - 1)) / T
    S a s x =
      (x ^ (-s):ℝ) * ∑' (n : ℕ+), a n * (x / (n ^ s : ℝ)) * I' lambda ((T / (2 * π)) * log (n / x)) := by
      -- Wait, there's a mistake. We can actually prove the opposite.
      negate_state;
      -- Proof starts here:
      -- Let's choose the sequence $a_n = 1$ for all $n$.
      use fun n => 1;
      -- Let's choose $s = 0$.
      use 0;
      simp +decide [CH2.S, CH2.I'];
      refine' ⟨ -1, 1, _, _ ⟩ <;> norm_num [ div_eq_mul_inv, mul_assoc, mul_comm, mul_left_comm, Real.pi_ne_zero ];
      rw [ tsum_eq_single 1 ] <;> norm_num;
      · norm_num [ Nat.floor_of_nonpos ];
      · exact fun n hn => Real.log_pos <| mod_cast Ne.bot_lt hn

theorem S_eq_I_corrected (a : ℕ → ℝ) (s x T : ℝ) (hs : s ≠ 1) (hT : 0 < T) (hx : 0 < x) :
    let lambda := (2 * π * (s - 1)) / T
    CH2.S a s x =
      (x ^ (-s):ℝ) * ∑' (n : ℕ+), a n * (x / n) * CH2.I' lambda ((T / (2 * π)) * Real.log (n / x)) := by
        by_cases hs : s < 1;
        · -- For $s < 1$, we have $S s x = \sum_{n=1}^{\lfloor x \rfloor} a_n / n^s$.
          have hS_lt_1 : CH2.S a s x = ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, a n / (n ^ s : ℝ) := by
            exact if_pos hs;
          -- For $s < 1$, we have $S s x = \sum_{n=1}^{\lfloor x \rfloor} a_n / n^s$ and the right-hand side simplifies to the same sum.
          have h_rhs_lt_1 : x ^ (-s : ℝ) * ∑' n : ℕ+, a n * (x / n) * CH2.I' (2 * Real.pi * (s - 1) / T) ((T / (2 * Real.pi)) * Real.log (n / x)) = x ^ (-s : ℝ) * ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, a n * (x / n) * (x / n) ^ (s - 1) := by
            have h_rhs_lt_1 : x ^ (-s : ℝ) * ∑' n : ℕ+, a n * (x / n) * CH2.I' (2 * Real.pi * (s - 1) / T) ((T / (2 * Real.pi)) * Real.log (n / x)) = x ^ (-s : ℝ) * ∑' n : ℕ+, if n ≤ ⌊x⌋₊ then a n * (x / n) * (x / n) ^ (s - 1) else 0 := by
              congr with n ; split_ifs <;> simp_all +decide [ Real.rpow_def_of_pos, div_eq_mul_inv ];
              · unfold CH2.I'; ring_nf; norm_num [ Real.pi_pos.ne', hT.ne', hx.ne' ] ;
                field_simp;
                rw [ Real.log_div, Real.log_div ] <;> norm_num <;> ring <;> norm_num [ hx.ne', hT.ne' ];
                exact Or.inl fun h => False.elim <| h.not_le <| by nlinarith [ Real.log_le_log ( by positivity ) <| show ( n : ℝ ) ≤ x from le_trans ( Nat.cast_le.mpr ‹_› ) <| Nat.floor_le hx.le ] ;
              · refine Or.inr ?_;
                refine' if_neg _;
                field_simp;
                exact not_le_of_gt ( mul_neg_of_neg_of_pos ( sub_neg_of_lt hs ) ( Real.log_pos ( by rw [ lt_div_iff₀ hx ] ; linarith [ Nat.lt_of_floor_lt ‹_› ] ) ) );
            rw [ h_rhs_lt_1, tsum_eq_sum ];
            any_goals exact Finset.Icc 1 ⟨ ⌊x⌋₊ + 1, Nat.succ_pos _ ⟩;
            · rw [ ← Finset.sum_filter ];
              field_simp;
              refine' Finset.sum_bij ( fun n hn => n ) _ _ _ _ <;> simp +decide [ mul_assoc, mul_comm, mul_left_comm ];
              · exact fun n hn₁ hn₂ => ⟨ PNat.one_le _, hn₂ ⟩;
              · exact fun b hb₁ hb₂ => ⟨ ⟨ b, hb₁ ⟩, ⟨ Nat.le_succ_of_le hb₂, hb₂ ⟩, rfl ⟩;
            · simp +zetaDelta at *;
              exact fun n hn₁ hn₂ => False.elim <| hn₁.not_le <| Nat.le_succ_of_le hn₂;
          simp_all +decide [ Real.rpow_sub hx, Real.rpow_neg hx.le, div_eq_mul_inv, mul_assoc, mul_comm, mul_left_comm, Finset.mul_sum _ _ _ ];
          refine Finset.sum_congr rfl fun n hn => ?_;
          rw [ Real.mul_rpow ( by positivity ) ( by positivity ), Real.inv_rpow ( by positivity ) ] ; ring;
          field_simp;
          rw [ Real.rpow_add hx, Real.rpow_neg_one ] ; ring;
          rw [ Real.rpow_add ( by norm_cast; linarith [ Finset.mem_Icc.mp hn ] ), Real.rpow_neg_one ] ; ring ; norm_num [ hx.ne' ];
          by_cases hn : n = 0 <;> aesop;
        · -- Since $s > 1$, we can use the definition of $S$ for $s > 1$.
          have hs_def : CH2.S a s x = ∑' n : ℕ, if n ≥ x then a n / (n ^ s : ℝ) else 0 := by
            unfold CH2.S; aesop;
          -- Since $s > 1$, we can rewrite the sum as $\sum_{n \geq x} a_n / n^s$.
          have hs_ge : ∑' n : ℕ, (if n ≥ x then a n / (n ^ s : ℝ) else 0) = ∑' n : ℕ+, (if (n : ℝ) ≥ x then a n / (n ^ s : ℝ) else 0) := by
            rw [ tsum_eq_tsum_of_ne_zero_bij ];
            use fun n => n.val;
            · aesop_cat;
            · intro n hn; use ⟨ ⟨ n, Nat.pos_of_ne_zero fun h => by aesop ⟩, by aesop ⟩ ; aesop;
            · aesop;
          -- Since $s > 1$, we can rewrite the sum as $\sum_{n \geq x} a_n / n^s$ and factor out $x^{-s}$.
          have hs_factor : ∑' n : ℕ+, (if (n : ℝ) ≥ x then a n / (n ^ s : ℝ) else 0) = x ^ (-s) * ∑' n : ℕ+, (if (n : ℝ) ≥ x then a n * (x / (n : ℝ)) * (x / (n : ℝ)) ^ (s - 1) else 0) := by
            rw [ ← tsum_mul_left ] ; congr ; ext n ; split_ifs <;> simp_all +decide [ div_eq_mul_inv, Real.rpow_sub_one, mul_assoc, mul_comm, mul_left_comm, hx.ne' ] ; ring;
            rw [ Real.mul_rpow ( by positivity ) ( by positivity ), Real.inv_rpow ( by positivity ), Real.rpow_neg ( by positivity ) ] ; ring;
            rw [ mul_assoc, mul_inv_cancel₀ ( by positivity ), mul_one ];
          convert hs_factor using 3;
          · rw [hs_def, hs_ge];
          · ext n; unfold CH2.I'; split_ifs <;> simp_all +decide [ Real.rpow_def_of_pos, div_pos, Real.pi_pos ] ;
            · rw [ Real.log_div ( by positivity ) ( by positivity ) ] ; ring_nf ; norm_num [ Real.pi_pos.ne', hT.ne', hx.ne' ] ;
              exact Or.inl ( by rw [ Real.log_mul ( by positivity ) ( by positivity ), Real.log_inv ] ; norm_num [ mul_assoc, mul_comm Real.pi _, Real.pi_ne_zero ] ; ring );
            · exact False.elim <| ‹0 ≤ 2 * Real.pi * ( s - 1 ) / T * ( T / ( 2 * Real.pi ) * Real.log ( ( n : ℝ ) / x ) ) ›.not_lt <| mul_neg_of_pos_of_neg ( div_pos ( mul_pos ( mul_pos two_pos Real.pi_pos ) <| sub_pos.mpr <| lt_of_le_of_ne hs <| Ne.symm ‹_› ) hT ) <| mul_neg_of_pos_of_neg ( div_pos hT <| mul_pos two_pos Real.pi_pos ) <| Real.log_neg ( div_pos ( Nat.cast_pos.mpr n.pos ) hx ) <| by rw [ div_lt_iff₀ hx ] ; linarith;
            · exact False.elim <| ‹2 * Real.pi * ( s - 1 ) / T * ( T / ( 2 * Real.pi ) * Real.log ( n / x ) ) < 0›.not_le <| mul_nonneg ( div_nonneg ( mul_nonneg ( by positivity ) <| sub_nonneg.mpr hs ) <| by positivity ) <| mul_nonneg ( div_nonneg ( by positivity ) <| by positivity ) <| Real.log_nonneg <| by rw [ le_div_iff₀ hx ] ; linarith;

[Terence Tao]

OK, the first proof is using CH2.S_eq_I, which is false, to prove everything. Implementing the fix for CH2.S_eq_I should resolve the issue.

[Pietro Monticone]

Ok, I'll open a PR soon.

[Terence Tao]

Aristotle needs a way to condense a very verbose proof based on contradictory hypotheses to a streamlined proof that some minimal set of hypotheses imply False. I could isolate the issue by copying the proof into my local IDE and tracing it through the infoview as it kept proving one absurd statement after another, but it would be nice to have that process be more automated.