name

formal source

  35
  36namespace KernelFamily
  37
  38def name : KernelFamily → String
  39  | constant_kernel  => "K1 (constant)"
  40  | inv_one_plus_z   => "K2 (1/(1+z))"
  41  | exponential      => "K3 (exp(-z/z0))"
  42
  43end KernelFamily
  44
  45/-- The BIT kernel function. -/
  46def kernel (k : KernelFamily) (z : ℝ) (z0 : ℝ := 1) : ℝ :=
  47  match k with
  48  | KernelFamily.constant_kernel  => 1
  49  | KernelFamily.inv_one_plus_z   => 1 / (1 + z)
  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 : ℝ) :