`KernelFamily`

definition

show as: view math explainer →

module: IndisputableMonolith.Cosmology.BITKernelFamilies
domain: Cosmology
line: 30 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cosmology.BITKernelFamilies on GitHub at line 30.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  27noncomputable section
  28
  29/-- Kernel family tag. -/
  30inductive KernelFamily where
  31  | constant_kernel
  32  | inv_one_plus_z
  33  | exponential
  34  deriving DecidableEq, Inhabited
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.