pith. machine review for the scientific record. sign in
theorem proved tactic proof

V_ub_match

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 134theorem V_ub_match : abs (V_ub_pred - V_ub_exp) < V_ub_err := by

proof body

Tactic-mode proof.

 135  have h_alpha_lower := alpha_lower_bound
 136  have h_alpha_upper := alpha_upper_bound
 137  simp only [V_ub_pred, V_ub_exp, V_ub_err, fine_structure_leakage]
 138  -- alpha/2 ∈ (0.003645, 0.003655)
 139  have h_lower : (0.003645 : ℝ) < Constants.alpha / 2 := by linarith
 140  have h_upper : Constants.alpha / 2 < (0.003655 : ℝ) := by linarith
 141  -- |alpha/2 - 0.00369| ≤ max(|0.003645 - 0.00369|, |0.003655 - 0.00369|)
 142  --                     = max(0.000045, 0.000035) = 0.000045 < 0.00011
 143  rw [abs_lt]
 144  constructor <;> linarith
 145
 146/-- Bounds on phi^(-3) needed for V_us proof.
 147    φ^(-3) ≈ 0.2360679...
 148
 149    These bounds are derived from phi_tight_bounds via antitonicity. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (15)

Lean names referenced from this declaration's body.