Ramanujan.Calculations.C1_le_one_of

theorem C1_le_one_of    {a : ℝ → ℝ} {xₐ : ℝ}    (hxₐ : xₐ = exp (3914 : ℝ))    (h2xa : 2 ≤ xₐ)    (h3870le : exp 3870 ≤ xₐ)    (ha_int : IntegrableOn (fun t ↦ a t / log t ^ 7) (Set.Icc 2 xₐ) volume)    (ha_le_low_huge : ∀ t ∈ Set.Icc 2 (exp 3870), a t ≤ (100000000000000000000 : ℝ))    (ha_mono_3000 : AntitoneOn a (Set.Ici (exp 3000)))    (ha_3870_upper : a (exp 3870) ≤ (1800 : ℝ))    (hJ3870 :      ∫ t in Set.Icc 2 (exp 3870), 1 / log t ^ 7        ≤ exp 3870 / log (exp 3870) ^ 7          + 7 * (sqrt (exp 3870) / log 2 ^ 8            + 2 ^ 8 * exp 3870 / log (exp 3870) ^ 8)) :    log xₐ ^ 6 / xₐ * ∫ t in Set.Icc 2 xₐ, (720 + a t) / log t ^ 7 ≤ (1 : ℝ) := by  let K : ℝ := (100000000000000000720 : ℝ)  have hK_nonneg : 0 ≤ K := by    dsimp [K]    positivity  let f : ℝ → ℝ := fun t ↦ (720 + a t) / log t ^ 7  have hJ_int : IntegrableOn (fun t : ℝ ↦ 1 / log t ^ 7) (Set.Icc 2 xₐ) volume :=    ContinuousOn.integrableOn_Icc (continuousOn_const.div (ContinuousOn.pow      (continuousOn_log.mono <| by        intro t ht        exact ne_of_gt (lt_of_lt_of_le (by norm_num) ht.1)) _) (by      intro t ht      exact pow_ne_zero _ <| ne_of_gt <| log_pos <| by linarith [ht.1]))  have hconst_int : IntegrableOn (fun t : ℝ ↦ (720 : ℝ) / log t ^ 7) (Set.Icc 2 xₐ) volume := by    have htmp : IntegrableOn (fun t : ℝ ↦ (720 : ℝ) * (1 / log t ^ 7)) (Set.Icc 2 xₐ) volume :=      hJ_int.const_mul 720    refine (integrableOn_congr_fun ?_ measurableSet_Icc).2 htmp    intro t ht    ring  have hadd_int : IntegrableOn (fun t : ℝ ↦ (720 : ℝ) / log t ^ 7 + a t / log t ^ 7) (Set.Icc 2 xₐ) volume :=    hconst_int.add ha_int  have hf_int : IntegrableOn f (Set.Icc 2 xₐ) volume := by    refine (integrableOn_congr_fun ?_ measurableSet_Icc).2 hadd_int    intro t ht    dsimp [f]    ring  have hsplit :      ∫ t in Set.Icc 2 xₐ, f t        = (∫ t in Set.Icc 2 (exp 3870), f t)          + (∫ t in Set.Icc (exp 3870) xₐ, f t) :=    integral_Icc_split (f := f) (a := 2) (b := exp 3870) (c := xₐ)      (by linarith [add_one_le_exp (3870 : ℝ)]) h3870le hf_int   have hf_int_low : IntegrableOn f (Set.Icc 2 (exp 3870)) volume :=    hf_int.mono_set (by intro t ht; exact ⟨ht.1, le_trans ht.2 h3870le⟩)  have hlow_rhs_int : IntegrableOn (fun t : ℝ ↦ K / log t ^ 7) (Set.Icc 2 (exp 3870)) volume := by    have htmp : IntegrableOn (fun t : ℝ ↦ K * (1 / log t ^ 7)) (Set.Icc 2 (exp 3870)) volume :=      (ContinuousOn.integrableOn_Icc (continuousOn_const.div (ContinuousOn.pow        (continuousOn_log.mono <| by          intro t ht          exact ne_of_gt (lt_of_lt_of_le (by norm_num) ht.1)) _) (by        intro t ht        exact pow_ne_zero _ <| ne_of_gt <| log_pos <| by linarith [ht.1]))).const_mul K    refine (integrableOn_congr_fun ?_ measurableSet_Icc).2 htmp    intro t ht    ring  have hlow_pt : ∀ t ∈ Set.Icc 2 (exp 3870), f t ≤ K / log t ^ 7 := by    intro t ht    have ha_le : a t ≤ (100000000000000000000 : ℝ) := ha_le_low_huge t ht    have hnum_le : 720 + a t ≤ K := by      dsimp [K]      linarith    have hlog_nonneg : 0 ≤ log t := log_nonneg (by linarith [ht.1])    dsimp [f]    exact div_le_div_of_nonneg_right hnum_le (pow_nonneg hlog_nonneg 7)  have hlow_le_rhs :      ∫ t in Set.Icc 2 (exp 3870), f t        ≤ ∫ t in Set.Icc 2 (exp 3870), K / log t ^ 7 :=    MeasureTheory.setIntegral_mono_on hf_int_low hlow_rhs_int measurableSet_Icc hlow_pt  have hlow_factor :      ∫ t in Set.Icc 2 (exp 3870), K / log t ^ 7        = K * ∫ t in Set.Icc 2 (exp 3870), 1 / log t ^ 7 := by    rw [← MeasureTheory.integral_const_mul]    refine MeasureTheory.setIntegral_congr_fun measurableSet_Icc ?_    intro t ht    ring  have hlow_le :      ∫ t in Set.Icc 2 (exp 3870), f t        ≤ K * (exp 3870 / log (exp 3870) ^ 7          + 7 * (sqrt (exp 3870) / log 2 ^ 8 + 2 ^ 8 * exp 3870 / log (exp 3870) ^ 8)) := by    rw [hlow_factor] at hlow_le_rhs    exact le_trans hlow_le_rhs (mul_le_mul_of_nonneg_left hJ3870 hK_nonneg)   have hf_int_high : IntegrableOn f (Set.Icc (exp 3870) xₐ) volume :=    hf_int.mono_set (by intro t ht; exact ⟨le_trans (by linarith [add_one_le_exp (3870 : ℝ)]) ht.1, ht.2⟩)  have hconst_high_int : IntegrableOn (fun _ : ℝ ↦ (2520 : ℝ) / (3870 : ℝ) ^ 7) (Set.Icc (exp 3870) xₐ) volume :=    ContinuousOn.integrableOn_Icc continuousOn_const  have hhigh_pt : ∀ t ∈ Set.Icc (exp 3870) xₐ, f t ≤ (2520 : ℝ) / (3870 : ℝ) ^ 7 := by    intro t ht    have ht3000 : exp 3000 ≤ t :=      le_trans (exp_le_exp.mpr (by norm_num : (3000 : ℝ) ≤ 3870)) ht.1    have hat3870 : a t ≤ a (exp 3870) :=      ha_mono_3000        (Set.mem_Ici.mpr (exp_le_exp.mpr (by norm_num : (3000 : ℝ) ≤ 3870)))        (Set.mem_Ici.mpr ht3000) ht.1    have hat : a t ≤ 1800 := le_trans hat3870 ha_3870_upper    have hnum_le : 720 + a t ≤ 2520 := by linarith    have hlog_ge : (3870 : ℝ) ≤ log t := by      have h := log_le_log (by positivity : (0 : ℝ) < exp 3870) ht.1      simpa [log_exp] using h    have hpow : (3870 : ℝ) ^ 7 ≤ log t ^ 7 := pow_le_pow_left₀ (by norm_num) hlog_ge 7    have hlog_nonneg : 0 ≤ log t := by linarith [hlog_ge]    calc      f t = (720 + a t) / log t ^ 7 := rfl      _ ≤ (2520 : ℝ) / log t ^ 7 := by        exact div_le_div_of_nonneg_right hnum_le (pow_nonneg hlog_nonneg 7)      _ ≤ (2520 : ℝ) / (3870 : ℝ) ^ 7 := by        exact div_le_div_of_nonneg_left (by norm_num : 0 ≤ (2520 : ℝ)) (by positivity) hpow  have hhigh_le_const :      ∫ t in Set.Icc (exp 3870) xₐ, f t        ≤ ∫ t in Set.Icc (exp 3870) xₐ, (2520 : ℝ) / (3870 : ℝ) ^ 7 :=    MeasureTheory.setIntegral_mono_on hf_int_high hconst_high_int measurableSet_Icc hhigh_pt  have hhigh_const_eval :      ∫ t in Set.Icc (exp 3870) xₐ, (2520 : ℝ) / (3870 : ℝ) ^ 7        = (2520 : ℝ) / (3870 : ℝ) ^ 7 * (xₐ - exp 3870) := by    rw [MeasureTheory.integral_Icc_eq_integral_Ioc,      ← intervalIntegral.integral_of_le h3870le,      intervalIntegral.integral_const]    simp [smul_eq_mul, mul_comm]  have hhigh_le :      ∫ t in Set.Icc (exp 3870) xₐ, f t        ≤ (2520 : ℝ) / (3870 : ℝ) ^ 7 * xₐ :=    le_trans (by simpa [hhigh_const_eval] using hhigh_le_const)      (mul_le_mul_of_nonneg_left (by linarith [show (0 : ℝ) ≤ exp 3870 by positivity])        (by positivity))   have hmain :      log xₐ ^ 6 / xₐ *          ((∫ t in Set.Icc 2 (exp 3870), f t) + (∫ t in Set.Icc (exp 3870) xₐ, f t))        ≤ log xₐ ^ 6 / xₐ *            (K * (exp 3870 / log (exp 3870) ^ 7              + 7 * (sqrt (exp 3870) / log 2 ^ 8 + 2 ^ 8 * exp 3870 / log (exp 3870) ^ 8))              + (2520 : ℝ) / (3870 : ℝ) ^ 7 * xₐ) :=    mul_le_mul_of_nonneg_left (by linarith [hlow_le, hhigh_le]) (by positivity)  have hmain' :      (3914 : ℝ) ^ 6 / exp (3914 : ℝ) *          ((∫ t in Set.Icc 2 (exp 3870), f t) + (∫ t in Set.Icc (exp 3870) (exp (3914 : ℝ)), f t))        ≤ (3914 : ℝ) ^ 6 / exp (3914 : ℝ) *          (K * (exp 3870 / (3870 : ℝ) ^ 7            + 7 * (sqrt (exp 3870) / log 2 ^ 8 + 2 ^ 8 * exp 3870 / (3870 : ℝ) ^ 8))            + (2520 : ℝ) / (3870 : ℝ) ^ 7 * exp (3914 : ℝ)) := by    simpa [hxₐ, log_exp] using hmain  have hdecomp :      (3914 : ℝ) ^ 6 / exp (3914 : ℝ) *          (K * (exp 3870 / (3870 : ℝ) ^ 7            + 7 * (sqrt (exp 3870) / log 2 ^ 8 + 2 ^ 8 * exp 3870 / (3870 : ℝ) ^ 8))            + (2520 : ℝ) / (3870 : ℝ) ^ 7 * exp (3914 : ℝ))        = (3914 : ℝ) ^ 6 / exp (3914 : ℝ) *            (K * (exp 3870 / (3870 : ℝ) ^ 7              + 7 * (sqrt (exp 3870) / log 2 ^ 8 + 2 ^ 8 * exp 3870 / (3870 : ℝ) ^ 8)))          + (2520 : ℝ) * (3914 : ℝ) ^ 6 / (3870 : ℝ) ^ 7 := by    field_simp  rw [hdecomp] at hmain'; dsimp [K] at hmain'  have hfin :      (3914 : ℝ) ^ 6 / exp (3914 : ℝ) *          ((100000000000000000720 : ℝ) *            (exp 3870 / (3870 : ℝ) ^ 7              + 7 *                (sqrt (exp 3870) / (log 2) ^ 8                  + (2 : ℝ) ^ 8 * exp 3870 / (3870 : ℝ) ^ 8)))          + (2520 : ℝ) * (3914 : ℝ) ^ 6 / (3870 : ℝ) ^ 7 ≤ 1 := by    nlinarith [low_contrib_raw_le_three_tenths,      show (2520 : ℝ) * (3914 : ℝ) ^ 6 / (3870 : ℝ) ^ 7 ≤ (7 : ℝ) / 10 by norm_num]  exact le_trans (by rw [hsplit]; simpa [f, hxₐ, log_exp] using hmain') hfin