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

weight_rs_positive

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)

  82theorem weight_rs_positive (t_ratio : ℝ) (ht : 0 < t_ratio) :
  83    1 < weight_rs t_ratio := by

proof body

Tactic-mode proof.

  84  unfold weight_rs
  85  have h1 : 0 < C_lag_RS * t_ratio ^ alpha_RS := by
  86    apply mul_pos
  87    · unfold C_lag_RS cLagLock
  88      -- φ^(-5) > 0 since φ > 0
  89      have h_phi_pos : 0 < Foundation.PhiForcing.φ := Foundation.PhiForcing.phi_pos
  90      exact Real.rpow_pos_of_pos h_phi_pos (-5)
  91    · exact rpow_pos_of_pos ht alpha_RS
  92  linarith
  93
  94/-- First-order lensing approximation for small weights.
  95    When w ≈ 1 + ε with ε small, lensing corrections are O(ε). -/

depends on (6)

Lean names referenced from this declaration's body.