inv_4pi_lower_v2

formal source

 860
 861/-! ### Phase 1: Tighter intermediate bounds -/
 862
 863lemma inv_4pi_lower_v2 : (0.07957 : ℝ) < 1 / (4 * Real.pi) := by
 864  have h_pi_lt : Real.pi < (3.141593 : ℝ) := pi_lt_d6_local
 865  have h_4pi_pos : (0 : ℝ) < 4 * Real.pi := by positivity
 866  calc (0.07957 : ℝ) < 1 / (4 * 3.141593) := by norm_num
 867    _ < 1 / (4 * Real.pi) := by
 868        apply one_div_lt_one_div_of_lt h_4pi_pos
 869        apply mul_lt_mul_of_pos_left h_pi_lt; norm_num
 870
 871lemma inv_4pi_upper_v2 : 1 / (4 * Real.pi) < (0.07958 : ℝ) := by
 872  have h_pi_gt : (3.141592 : ℝ) < Real.pi := pi_gt_d6_local
 873  have h_lower_pos : (0 : ℝ) < 4 * 3.141592 := by norm_num
 874  calc 1 / (4 * Real.pi) < 1 / (4 * 3.141592) := by
 875        apply one_div_lt_one_div_of_lt h_lower_pos
 876        apply mul_lt_mul_of_pos_left h_pi_gt; norm_num
 877    _ < (0.07958 : ℝ) := by norm_num
 878
 879lemma step_e_mu_bounds_v2 : (11.0795 : ℝ) < step_e_mu ∧ step_e_mu < (11.0796 : ℝ) := by
 880  simp only [step_e_mu]; rw [E_passive_exact]
 881  have h_inv_lo := inv_4pi_lower_v2
 882  have h_inv_hi := inv_4pi_upper_v2
 883  have h_alpha := alpha_sq_bounds
 884  constructor <;> linarith
 885
 886lemma step_mu_tau_bounds_v2 : (5.8649 : ℝ) < step_mu_tau ∧ step_mu_tau < (5.8651 : ℝ) := by
 887  simp only [step_mu_tau, W_exact, AlphaDerivation.D, cube_faces]
 888  have h_alpha := alpha_bounds
 889  constructor <;> nlinarith
 890
 891lemma predicted_residue_mu_bounds_v2 :
 892    (-9.6268 : ℝ) < predicted_residue_mu ∧ predicted_residue_mu < (-9.6254 : ℝ) := by
 893  simp only [predicted_residue_mu]