constant_kernel_eq_one

formal source

  55  cases k <;> simp [kernel]
  56
  57/-- The constant kernel is `1` everywhere. -/
  58theorem constant_kernel_eq_one (z z0 : ℝ) :
  59    kernel KernelFamily.constant_kernel z z0 = 1 := rfl
  60
  61/-- The 1/(1+z) kernel is positive for `z > -1`. -/
  62theorem inv_one_plus_z_pos (z : ℝ) (h : -1 < z) (z0 : ℝ) :
  63    0 < kernel KernelFamily.inv_one_plus_z z z0 := by
  64  unfold kernel
  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