`beta_bound_small`

proved

show as: view math explainer →

module: IndisputableMonolith.Relativity.ILG.PPN
domain: Relativity
line: 56 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Relativity.ILG.PPN on GitHub at line 56.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  53    _ ≤ (1/10) * κ := by exact mul_le_mul_of_nonneg_left h (by norm_num)
  54
  55/-- Bound: if |C_lag·α| ≤ κ then |β−1| ≤ (1/20) κ. -/
  56theorem beta_bound_small (C_lag α κ : ℝ)
  57  (h : |C_lag * α| ≤ κ) :
  58  |beta_lin C_lag α - 1| ≤ (1/20 : ℝ) * κ := by
  59  unfold beta_lin
  60  simp only [add_sub_cancel_left]
  61  rw [abs_mul]
  62  calc |1/20| * |C_lag * α| = (1/20) * |C_lag * α| := by norm_num
  63    _ ≤ (1/20) * κ := by exact mul_le_mul_of_nonneg_left h (by norm_num)
  64
  65end PPN
  66end ILG
  67end Relativity
  68end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.