kernel_at_zero

formal source

  50  | KernelFamily.exponential      => Real.exp (- z / z0)
  51
  52/-- All three kernels equal 1 at `z = 0`. -/
  53theorem kernel_at_zero (k : KernelFamily) (z0 : ℝ) :
  54    kernel k 0 z0 = 1 := by
  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