FKS2.integral_term_bound

We obtain our final bound for converting bounds on $E_\theta$ to bounds on $E_\pi$. -/

/- The following lemmas are used for theorem_3. -/

-- Helper: admissible_bound is linear in A lemma admissible_bound_mul (A K B C R x : ℝ) : admissible_bound (A * K) B C R x = K * admissible_bound A B C R x := by simp [admissible_bound]; ring

/- Helper: the ratio log x / (x * admissible_bound A B C R x) equals R^B / A * g_bound 1 (1-B) (C/√R) x -/ lemma ratio_eq_g {A B C R x : ℝ} (hR : R > 0) (hx : x > 0) (hlogx : log x > 0) : log x / (x * admissible_bound A B C R x) = R ^ B / A * g_bound 1 (1 - B) (C / sqrt R) x := by unfold admissible_bound g_bound; ring_nf; rw [ Real.mul_rpow ( by positivity ) ( by positivity ), Real.inv_rpow ( by positivity ) ] ; norm_num [ Real.rpow_sub, Real.rpow_neg, Real.sqrt_mul, hR.le, hx.le, hlogx.le ] ; ring_nf; rw [ Real.rpow_sub hlogx, Real.rpow_one ] ; norm_num [ Real.exp_neg ] ; ring_nf; next => norm_num left rw [show (log x * R⁻¹) ^ (1 / 2 : ℝ) = Real.sqrt (log x * R⁻¹) by rw [Real.sqrt_eq_rpow]] rw [Real.sqrt_mul, Real.sqrt_inv] <;> linarith

/- Helper: for x ≥ x₁, the ratio log x / (x * admissible_bound) is at most the value at x₁ -/ lemma ratio_mono {A B C R x₁ x : ℝ} (hB : B ≥ 1 + C ^ 2 / (16 * R)) (hR : R > 0) (hx1 : x₁ > 1) (hx : x ≥ x₁) (hA : A > 0) : log x / (x * admissible_bound A B C R x) ≤ log x₁ / (x₁ * admissible_bound A B C R x₁) := by have h_ratio_simplified : R ^ B / A * g_bound 1 (1 - B) (C / Real.sqrt R) x ≤ R ^ B / A * g_bound 1 (1 - B) (C / Real.sqrt R) x₁ := by have h_decreasing : ∀ x y : ℝ, 1 < x → x ≤ y → g_bound 1 (1 - B) (C / Real.sqrt R) x ≥ g_bound 1 (1 - B) (C / Real.sqrt R) y := by intros x y hx hy have h_deriv_neg : ∀ x : ℝ, 1 < x → deriv (g_bound 1 (1 - B) (C / Real.sqrt R)) x ≤ 0 := by intros x hx have h_deriv_neg : deriv (g_bound 1 (1 - B) (C / Real.sqrt R)) x = (-1 * Real.log x + (1 - B) + (C / (2 * Real.sqrt R)) * Real.sqrt (Real.log x)) * x ^ (-2 : ℝ) * (Real.log x) ^ ((1 - B) - 1) * Real.exp ((C / Real.sqrt R) * Real.sqrt (Real.log x)) := by field_simp; rw [ lemma_10_substep hx ] ; ring_nf ; norm_num [ Real.sqrt_ne_zero'.mpr hR, Real.sqrt_ne_zero'.mpr ( Real.log_pos hx ), Real.rpow_neg_one ] ; ring_nf; grind generalize_proofs at *; ( have h_quad_neg : ∀ u : ℝ, u > 0 → -u^2 + (C / (2 * Real.sqrt R)) * u + (1 - B) ≤ 0 := by intros u hu have h_quad_neg : -u^2 + (C / (2 * Real.sqrt R)) * u + (1 - B) ≤ 0 := by have h_discriminant : (C / (2 * Real.sqrt R))^2 - 4 * (-1) * (1 - B) ≤ 0 := by field_simp at *; ring_nf at *; nlinarith [ inv_mul_cancel₀ ( ne_of_gt hR ), inv_pos.mpr hR, Real.sqrt_nonneg R, Real.sq_sqrt hR.le, mul_inv_cancel₀ ( ne_of_gt ( Real.sqrt_pos.mpr hR ) ), Real.sqrt_nonneg ( R⁻¹ ), Real.sq_sqrt ( inv_nonneg.mpr hR.le ) ] ; linarith [ sq_nonneg ( C / ( 2 * Real.sqrt R ) - 2 * u ) ] generalize_proofs at *; (exact h_quad_neg) generalize_proofs at *; ( exact h_deriv_neg.symm ▸ mul_nonpos_of_nonpos_of_nonneg ( mul_nonpos_of_nonpos_of_nonneg ( mul_nonpos_of_nonpos_of_nonneg ( by have := h_quad_neg ( Real.sqrt ( Real.log x ) ) ( Real.sqrt_pos.mpr ( Real.log_pos hx ) ) ; rw [ Real.sq_sqrt ( Real.log_nonneg hx.le ) ] at this; linarith ) ( by positivity ) ) ( by exact Real.rpow_nonneg ( Real.log_nonneg hx.le ) _ ) ) ( by positivity ) ;)) generalize_proofs at *; ( by_contra h_contra; have := exists_deriv_eq_slope ( g_bound 1 ( 1 - B ) ( C / Real.sqrt R ) ) ( show x < y from hy.lt_of_ne ( by rintro rfl; linarith ) ) ; norm_num at this; exact absurd ( this ( by exact ContinuousOn.mono ( show ContinuousOn ( g_bound 1 ( 1 - B ) ( C / Real.sqrt R ) ) ( Set.Icc x y ) from by exact ContinuousOn.mul ( ContinuousOn.mul ( ContinuousOn.rpow continuousOn_id continuousOn_const <| by intro u hu; exact Or.inl <| by linarith [ hu.1 ] ) <| ContinuousOn.rpow ( Real.continuousOn_log.mono <| by exact fun u hu => ne_of_gt <| by linarith [ hu.1 ] ) continuousOn_const <| by intro u hu; exact Or.inl <| ne_of_gt <| Real.log_pos <| by linarith [ hu.1 ] ) <| ContinuousOn.rexp <| ContinuousOn.mul continuousOn_const <| ContinuousOn.sqrt <| Real.continuousOn_log.mono <| by exact fun u hu => ne_of_gt <| by linarith [ hu.1 ] ) <| Set.Icc_subset_Icc ( by linarith ) le_rfl ) <| by exact fun u hu => DifferentiableAt.differentiableWithinAt <| by exact DifferentiableAt.mul ( DifferentiableAt.mul ( DifferentiableAt.rpow ( differentiableAt_id ) ( differentiableAt_const _ ) <| by linarith [ hu.1 ] ) <| DifferentiableAt.rpow ( Real.differentiableAt_log <| by linarith [ hu.1 ] ) ( differentiableAt_const _ ) <| by exact ne_of_gt <| Real.log_pos <| by linarith [ hu.1 ] ) <| DifferentiableAt.exp <| DifferentiableAt.mul ( differentiableAt_const _ ) <| DifferentiableAt.sqrt ( Real.differentiableAt_log <| by linarith [ hu.1 ] ) <| by exact ne_of_gt <| Real.log_pos <| by linarith [ hu.1 ] ) ( by rintro ⟨ c, ⟨ hxc, hcy ⟩, hcd ⟩ ; rw [ eq_div_iff ] at hcd <;> nlinarith [ h_deriv_neg c <| by linarith ] ) ;); exact mul_le_mul_of_nonneg_left ( h_decreasing _ _ hx1 hx ) ( by positivity ); convert h_ratio_simplified using 1 <;> norm_num [ ratio_eq_g hR ( by linarith : 0 < x ) ( Real.log_pos ( by linarith ) ), ratio_eq_g hR ( by linarith : 0 < x₁ ) ( Real.log_pos ( by linarith ) ) ]

/- Helper: for B ≥ 3/2 and x ≥ x₁ ≥ x₀, the m(x₀,x)*(log x)^(1-B) factor simplifies -/ lemma m_simplify {B x₀ x x₁ : ℝ} (hB : B ≥ 3 / 2) (hx₀ : x₀ > 1) (hx₁ : x₁ > 1) (hx₁x₀ : x₁ ≥ x₀) (hx : x ≥ x₁) (hlogx : log x > 0) : max ((log x₀) ^ ((2 * B - 3) / 2)) ((log x) ^ ((2 * B - 3) / 2)) * (log x) ^ (1 - B) ≤ 1 / sqrt (log x₁) := by rw [ max_def ]; split_ifs <;> norm_num [ Real.sqrt_eq_rpow, ← Real.rpow_add hlogx ]; · rw [ ← Real.rpow_neg ( Real.log_nonneg hx₁.le ) ] ; ring_nf ; norm_num [ hlogx ]; rw [ Real.rpow_le_rpow_iff_of_neg ] <;> linarith [ Real.log_pos hx₁, Real.log_le_log ( by linarith ) hx ]; · exact False.elim <| ‹¬log x₀ ^ ( ( 2 * B - 3 ) / 2 ) ≤ log x ^ ( ( 2 * B - 3 ) / 2 ) › <| Real.rpow_le_rpow ( Real.log_nonneg <| by linarith ) ( Real.log_le_log ( by linarith ) <| by linarith ) <| by linarith;

/- Helper: admissible_bound is positive under suitable conditions -/ lemma admissible_bound_pos {A B C R x : ℝ} (hA : A > 0) (hR : R > 0) (hlogx : log x > 0) : admissible_bound A B C R x > 0 := by exact mul_pos ( mul_pos hA ( Real.rpow_pos_of_pos ( div_pos hlogx hR ) _ ) ) ( Real.exp_pos _ )

/- Helper: Eθ is non-negative -/ lemma Eθ_nonneg (x : ℝ) (hx : x > 0) : Eθ x ≥ 0 := by exact div_nonneg ( abs_nonneg _ ) hx.le

/- Helper: δ is non-negative -/ lemma delta_nonneg (x₀ : ℝ) : δ x₀ ≥ 0 := by exact abs_nonneg _

/- Helper: from ratio_mono, derive the bound on log x / x in terms of admissible_bound -/ lemma logx_over_x_bound {A B C R x₁ x : ℝ} (hB : B ≥ 1 + C ^ 2 / (16 * R)) (hR : R > 0) (hA : A > 0) (hx1_gt1 : x₁ > 1) (hx : x ≥ x₁) : log x / x ≤ (log x₁ / (x₁ * admissible_bound A B C R x₁)) * admissible_bound A B C R x := by convert! mul_le_mul_of_nonneg_right ( ratio_mono hB hR hx1_gt1 hx hA ) ( admissible_bound_pos hA hR ( Real.log_pos <| show 1 < x by linarith ) |> le_of_lt ) using 1 ; ring_nf; norm_num [ ne_of_gt ( admissible_bound_pos hA hR ( Real.log_pos <| show 1 < x by linarith ) ) ]

/- PROBLEM Bound the delta term from eq_30.

PROVIDED SOLUTION Use logx_over_x_bound to get log x / x ≤ (log x₁ / (x₁ * admissible_bound A B C R x₁)) * admissible_bound A B C R x. Multiply both sides by (x₀ / log x₀) * δ x₀ (which is non-negative since δ is non-negative by delta_nonneg and x₀/log x₀ > 0 from hlogx₀). The LHS becomes (log x / x) * (x₀ / log x₀) * δ x₀. The RHS becomes (log x₁ / (x₁ * admissible_bound A B C R x₁)) * (x₀ / log x₀) * δ x₀ * admissible_bound A B C R x which equals (x₀ * log x₁) / (admissible_bound A B C R x₁ * x₁ * log x₀) * δ x₀ * admissible_bound A B C R x by algebraic rearrangement. -/ lemma delta_term_bound {A B C R x₀ x₁ x : ℝ} (hB : B ≥ 1 + C ^ 2 / (16 * R)) (hR : R > 0) (hA : A > 0) (hx1_gt1 : x₁ > 1) (hx : x ≥ x₁) (hx0_pos : x₀ > 0) (hlogx₀ : log x₀ > 0) : (log x / x) * (x₀ / log x₀) * δ x₀ ≤ (x₀ * log x₁) / (admissible_bound A B C R x₁ * x₁ * log x₀) * δ x₀ * admissible_bound A B C R x := by have h1 := logx_over_x_bound hB hR hA hx1_gt1 hx have h2 : x₀ / log x₀ ≥ 0 := div_nonneg hx0_pos.le hlogx₀.le have h3 := delta_nonneg x₀ calc (log x / x) * (x₀ / log x₀) * δ x₀ ≤ ((log x₁ / (x₁ * admissible_bound A B C R x₁)) * admissible_bound A B C R x) * (x₀ / log x₀) * δ x₀ := mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_right h1 h2) h3 _ = (x₀ * log x₁) / (admissible_bound A B C R x₁ * x₁ * log x₀) * δ x₀ * admissible_bound A B C R x := by ring

/- Helper: Dawson function is monotone decreasing for large arguments (after ~0.924) We use remark_after_corollary_11 which gives the existence of a maximum around 0.924 -/ lemma dawson_antitoneOn : ∃ x₀ : ℝ, x₀ < 1 ∧ StrictAntiOn dawson (Set.Ioi x₀) := by obtain ⟨ x₀, hx₀ ⟩ := remark_after_corollary_11; exact ⟨ x₀, by norm_num at hx₀; linarith, hx₀.2.2 ⟩

/- Helper: Eθ t = |Eθ t| since Eθ is non-negative -/ lemma Eθ_eq_abs {t : ℝ} (ht : t > 0) : Eθ t = |Eθ t| := by rw [ abs_of_nonneg ( Eθ_nonneg t ht ) ]

/- Algebraic identity: (log x / x) * (2A/R^B) * x * m * exp(-C*√(log x/R)) * D = 2 * m * (log x)^(1-B) * D * admissible_bound A B C R x -/ lemma integral_algebra {A B C R x m D : ℝ} (hR : R > 0) (hx : x > 1) : (log x / x) * ((2 * A) / R ^ B * x * m * exp (-C * √(log x / R)) * D) = 2 * m * (log x) ^ (1 - B) * D * admissible_bound A B C R x := by unfold admissible_bound; ring_nf; rw [ Real.rpow_sub ( by linarith [ Real.log_pos hx ] ), Real.rpow_one ] ; ring_nf; rw [ Real.mul_rpow ( by linarith [ Real.log_pos hx ] ) ( by positivity ), Real.inv_rpow ( by positivity ) ] ; ring_nf ; norm_num [ ne_of_gt ( zero_lt_one.trans hx ) ] ; rw [ mul_inv_cancel_right₀ ( ne_of_gt ( Real.rpow_pos_of_pos ( Real.log_pos hx ) _ ) ) ] have heq: Real.exp (-(C * (Real.log x * R⁻¹)^(1/2 : ℝ))) = Real.exp (-(C * Real.sqrt (Real.log x * R⁻¹))) := by congr; rw [Real.sqrt_eq_rpow] rw [heq] linarith

/- Dawson monotonicity for arguments ≥ 1 -/ lemma dawson_mono_ge_one {a b : ℝ} (ha : a ≥ 1) (hab : a ≤ b) : dawson b ≤ dawson a := by obtain ⟨ x₀, hx₀ ⟩ := dawson_antitoneOn; exact hx₀.2.le_iff_ge ( show x₀ < b by linarith ) ( show x₀ < a by linarith ) |>.2 ( by linarith )

/- Derive that √(log x₁) - C/(2√R) ≥ 1 from the hypothesis on x₁ -/ lemma sqrt_log_minus_ge_one {C R x₁ : ℝ} (hx1 : x₁ ≥ exp ((1 + C / (2 * sqrt R)) ^ 2)) : √(log x₁) - C / (2 * √R) ≥ 1 := by -- Taking the natural logarithm of both sides of the inequality $x₁ \geq \exp((1 + C / (2 * \sqrt{R}))^2)$, we get $\log x₁ \geq (1 + C / (2 * \sqrt{R}))^2$. have h_log : Real.log x₁ ≥ (1 + C / (2 * Real.sqrt R)) ^ 2 := by simpa using Real.log_le_log ( by positivity ) hx1; exact le_tsub_of_add_le_right ( Real.le_sqrt_of_sq_le ( by linarith ) )

/- PROBLEM Helper: the integral term from eq_30 is bounded by the Dawson component of μ_asymp

Bound the integral term from eq_30.

PROVIDED SOLUTION Step 1: Since Eθ t ≥ 0, we have ∫ Eθ t / log t^2 ≤ ∫ |Eθ t| / log t^2. Step 2: Apply lemma_12 to bound the integral. Step 3: Multiply by log x / x and use integral_algebra to simplify: = 2 * m(x₀,x) * (log x)^(1-B) * dawson(√(log x) - C/(2√R)) * admissible_bound. Step 4: Apply m_simplify to get m * (log x)^(1-B) ≤ 1/√(log x₁). Step 5: Apply dawson_mono_ge_one (using sqrt_log_minus_ge_one for the ≥ 1 condition) to get dawson(√(log x)-C/(2√R)) ≤ dawson(√(log x₁)-C/(2√R)). Step 6: Combine: ≤ 2/√(log x₁) * dawson(√(log x₁)-C/(2√R)) * admissible_bound.