exp_kernel_pos

formal source

  65  exact div_pos one_pos (by linarith)
  66
  67/-- The exponential kernel is positive everywhere. -/
  68theorem exp_kernel_pos (z z0 : ℝ) :
  69    0 < kernel KernelFamily.exponential z z0 := by
  70  unfold kernel
  71  exact Real.exp_pos _
  72
  73/-- The maximum BIT amplitude is `J(φ) = φ - 3/2 ≈ 0.118`. -/
  74def delta_w0_max : ℝ := phi - 3 / 2
  75
  76theorem delta_w0_max_pos : 0 < delta_w0_max := by
  77  unfold delta_w0_max
  78  have := phi_gt_onePointFive
  79  linarith
  80
  81theorem delta_w0_max_lt_one : delta_w0_max < 1 := by
  82  unfold delta_w0_max
  83  have := phi_lt_two
  84  linarith
  85
  86/-- The effective equation of state under BIT. -/
  87def w_eff (k : KernelFamily) (z delta_w0 : ℝ) (z0 : ℝ := 1) : ℝ :=
  88  -1 + delta_w0 * kernel k z z0
  89
  90/-- At `z = 0`, `w_eff = -1 + δw_0` for any kernel. -/
  91theorem w_eff_at_zero (k : KernelFamily) (delta_w0 z0 : ℝ) :
  92    w_eff k 0 delta_w0 z0 = -1 + delta_w0 := by
  93  unfold w_eff
  94  rw [kernel_at_zero]
  95  ring
  96
  97/-! ## Master certificate -/
  98