FKS2.theorem_6

@[blueprint  "fks2-theorem-6"  (title := "FKS2 Theorem 6")  (latexEnv := "theorem")  (discussion := 718)]theorem theorem_6 {x₀ x₁ : ℝ} (x₂ : EReal) (h : x₁ ≥ max x₀ 14)  {N : ℕ} (b : Fin (N + 1) → ℝ) (hmono : Monotone b)  (h_b_start : b 0 = log x₀)  (h_b_end : b (Fin.last N) = log x₁)  (εθ_num : ℝ → ℝ)  (h_εθ_num : ∀ i : Fin (N+1), Eθ.numericalBound (exp (b i)) εθ_num) (x : ℝ) (hx₁ : x₁ ≤ x) (hx₂ : x.toEReal ≤ x₂) (hx₀ : x₀ ≥ 2) :  Eπ x ≤ επ_num b εθ_num x₀ x₁ x₂ := by  -- NOTE: the hypothesis `hx₀ : x₀ ≥ 2` is not present in the original source material  have h_key : Eπ x ≤ εθ_num x₁ + (x₀ * log x₁) / (x₁ * log x₀) * δ x₀ + (log x₁ / x₁) * (∑ i ∈ Finset.Iio (Fin.last N), εθ_num (exp (b i)) * (Li (exp (b (i + 1))) - Li (exp (b i)) + exp (b i) / b i - exp (b (i + 1)) / b (i + 1))) + εθ_num x₁ * ((log x / x) * ∫ t in x₁..x, 1 / (Real.log t) ^ 2) := by    have h_key : Eπ x ≤ Eθ x + (log x / x) * (x₀ / log x₀) * δ x₀ + (log x / x) * (∫ t in x₀..x₁, Eθ t / log t ^ 2) + (log x / x) * (∫ t in x₁..x, Eθ t / log t ^ 2) := by      have h_split : ∫ t in x₀..x, Eθ t / log t ^ 2 = (∫ t in x₀..x₁, Eθ t / log t ^ 2) + (∫ t in x₁..x, Eθ t / log t ^ 2) := by        rw [ intervalIntegral.integral_add_adjacent_intervals ] <;> apply_rules [ Eθ_integrable ] <;> linarith [ le_max_left x₀ 14, le_max_right x₀ 14 ];      convert eq_30 ( show x ≥ x₀ by linarith [ le_max_left x₀ 14 ] ) ( show x₀ ≥ 2 by linarith ) using 1 ; rw [ h_split ] ; ring;    have h_bound : Eθ x ≤ εθ_num x₁ := by      have := h_εθ_num ( Fin.last N ) ; simp_all +decide [ Eθ.numericalBound ] ;      simpa [ Real.exp_log ( by linarith : 0 < x₁ ) ] using this x ( by rw [ Real.exp_log ( by linarith ) ] ; linarith )    have h_bound_integral : ∫ t in x₀..x₁, Eθ t / log t ^ 2 ≤ ∑ i ∈ Finset.Iio (Fin.last N), εθ_num (exp (b i)) * (Li (exp (b (i + 1))) - Li (exp (b i)) + exp (b i) / b i - exp (b (i + 1)) / b (i + 1)) := by      apply_rules [ bound_x0_x1 ];      linarith [ le_max_left x₀ 14, le_max_right x₀ 14 ]    have h_bound_integral_last : ∫ t in x₁..x, Eθ t / log t ^ 2 ≤ εθ_num x₁ * ∫ t in x₁..x, 1 / log t ^ 2 := by      apply_rules [ Eθ_bound_integral_last ];      · linarith [ le_max_left x₀ 14, le_max_right x₀ 14 ];      · convert h_εθ_num ( Fin.last N ) using 1 ; norm_num [ h_b_end, Real.exp_log ( show 0 < x₁ by linarith [ le_max_right x₀ 14 ] ) ];    have h_log_div_self_antitone : Real.log x / x ≤ Real.log x₁ / x₁ := by      apply Real.log_div_self_antitoneOn;      · exact le_trans ( Real.exp_one_lt_d9.le ) ( by norm_num; linarith [ le_max_right x₀ 14 ] );      · exact le_trans ( Real.exp_one_lt_d9.le ) ( by norm_num; linarith [ le_max_right x₀ 14 ] );      · linarith;    refine le_trans h_key ?_;    refine add_le_add ( add_le_add ( add_le_add h_bound ?_ ) ?_ ) ?_;    · convert mul_le_mul_of_nonneg_right ( mul_le_mul_of_nonneg_right h_log_div_self_antitone ( show 0 ≤ x₀ / log x₀ by exact div_nonneg ( by linarith ) ( Real.log_nonneg ( by linarith ) ) ) ) ( show 0 ≤ δ x₀ by exact delta_nonneg x₀ ) using 1 ; ring;    · gcongr;      · refine intervalIntegral.integral_nonneg ?_ ?_ <;> norm_num;        · linarith [ le_max_left x₀ 14, le_max_right x₀ 14 ];        · exact fun u hu₁ hu₂ => div_nonneg ( Eθ_nonneg u ( by linarith ) ) ( sq_nonneg _ );      · exact div_nonneg ( Real.log_nonneg ( by linarith [ le_max_right x₀ 14 ] ) ) ( by linarith [ le_max_right x₀ 14 ] );    · convert mul_le_mul_of_nonneg_left h_bound_integral_last ( show 0 ≤ log x / x by exact div_nonneg ( Real.log_nonneg ( by linarith [ le_max_left x₀ 14, le_max_right x₀ 14 ] ) ) ( by linarith [ le_max_left x₀ 14, le_max_right x₀ 14 ] ) ) using 1 ; ring;  by_cases hc : x₂ ≤ Real.toEReal ( x₁ * Real.log x₁ )  · simp_all +decide only [ge_iff_le, sup_le_iff, Fin.Iio_last_eq_map, Finset.sum_map,    Fin.coe_castSuccEmb, Fin.coeSucc_eq_succ, one_div, EReal.coe_mul, επ_num, μ_num, ↓reduceIte]    have h63 := theorem_6_3 ( by linarith : 14 ≤ x₁ ) x₂.toReal ( by      cases x₂ <;> norm_num at *;      · linarith;      · exact absurd hc ( by exact ne_of_lt ( EReal.coe_lt_top _ ) ) ) x hx₁ ( by      cases x₂ <;> norm_num at *;      · linarith;      · exact absurd hc ( by exact ne_of_lt ( EReal.coe_lt_top _ ) ) ) ( by      cases x₂ <;> norm_num at *;      · exact_mod_cast hc;      · exact mul_nonneg ( by linarith ) ( Real.log_nonneg ( by linarith ) ) );    unfold μ_num_1; ring_nf at *;    by_cases h : εθ_num x₁ = 0    · simp_all +decide only [mul_comm, inv_pow, mul_assoc, mul_left_comm, zero_mul, mul_zero,      add_zero, zero_add, Finset.sum_sub_distrib, inv_zero, Fin.Iio_last_eq_map, Finset.sum_map,      Fin.coe_castSuccEmb, Fin.coeSucc_eq_succ, sub_self, ge_iff_le];      have := exists_Eθ_pos ( x₁ := x₁ ) ; obtain ⟨ y, hy₁, hy₂ ⟩ := this; have := h_εθ_num ( Fin.last N ) ;      simp_all +decide only [gt_iff_lt, Real.exp_log (by linarith : 0 < x₁), ge_iff_le] ;      exact absurd ( this y hy₁ ) ( by norm_num [ h ] ; linarith );    · simp_all +decide [ mul_assoc, mul_comm, mul_left_comm ]      nlinarith [ show 0 < εθ_num x₁ from lt_of_le_of_ne ( by                    have := h_εθ_num ( Fin.last N );                    rw [ h_b_end, Real.exp_log ( by linarith ) ] at this; exact le_trans ( Eθ_nonneg _ ( by linarith ) ) ( this _ le_rfl ) ; ) ( Ne.symm h ) ];  · simp_all +decide only [ge_iff_le, sup_le_iff, Fin.Iio_last_eq_map, Finset.sum_map,    Fin.coe_castSuccEmb, Fin.coeSucc_eq_succ, one_div, EReal.coe_mul, not_le, επ_num, μ_num]    have h62 := theorem_6_2 ( by linarith : 14 ≤ x₁ ) x hx₁    simp_all +decide only [one_div, μ_num_2, Fin.Iio_last_eq_map, Finset.sum_map,      Fin.coe_castSuccEmb, Fin.coeSucc_eq_succ, ge_iff_le];    have hεθpos : 0 < εθ_num x₁ := by      have := exists_Eθ_pos ( x₁ := x₁ ) ; obtain ⟨ y, hy₁, hy₂ ⟩ := this; have := h_εθ_num ( Fin.last N ) y; simp_all +decide [ Real.exp_log ( by linarith : 0 < x₁ ) ] ;      linarith;    split_ifs    · simp_all +decide only [div_eq_mul_inv, mul_inv_rev, mul_comm, mul_left_comm, mul_assoc,      mul_add, mul_one, ge_iff_le];      exact absurd ‹_› ( not_le_of_gt hc );    · simp_all +decide [ mul_add, mul_assoc, mul_comm, mul_left_comm, div_eq_mul_inv ];      norm_num [ mul_left_comm ( εθ_num x₁ ), mul_assoc, hεθpos.ne' ];      nlinarith [ show 0 ≤ εθ_num x₁ by positivity ]