`kernel`

definition

show as: view math explainer →

module: IndisputableMonolith.ILG.Kernel
domain: ILG
line: 79 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.ILG.Kernel on GitHub at line 79.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  76  w(k, a) = 1 + C · (a / (k τ₀))^α
  77
  78We use max with a small ε to avoid division issues when k τ₀ = 0. -/
  79noncomputable def kernel (P : KernelParams) (k a : ℝ) : ℝ :=
  80  1 + P.C * (max 0.01 (a / (k * P.tau0))) ^ P.alpha
  81
  82/-- Simplified kernel when k = 1 (reference wavenumber). -/
  83noncomputable def kernelAtRefK (P : KernelParams) (a : ℝ) : ℝ :=
  84  1 + P.C * (max 0.01 (a / P.tau0)) ^ P.alpha
  85
  86@[simp] lemma kernelAtRefK_eq (P : KernelParams) (a : ℝ) :
  87    kernelAtRefK P a = kernel P 1 a := by
  88  simp [kernelAtRefK, kernel, one_mul]
  89
  90/-! ## Basic Properties -/
  91
  92/-- Kernel is always positive for valid parameters. -/
  93theorem kernel_pos (P : KernelParams) (k a : ℝ) : 0 < kernel P k a := by
  94  unfold kernel
  95  have hmax_pos : 0 < max 0.01 (a / (k * P.tau0)) := by
  96    apply lt_max_of_lt_left
  97    norm_num
  98  have hpow_nonneg : 0 ≤ (max 0.01 (a / (k * P.tau0))) ^ P.alpha :=
  99    Real.rpow_nonneg (le_of_lt hmax_pos) P.alpha
 100  have hcorr_nonneg : 0 ≤ P.C * (max 0.01 (a / (k * P.tau0))) ^ P.alpha :=
 101    mul_nonneg P.C_nonneg hpow_nonneg
 102  linarith
 103
 104/-- Kernel is at least 1. -/
 105theorem kernel_ge_one (P : KernelParams) (k a : ℝ) : 1 ≤ kernel P k a := by
 106  unfold kernel
 107  have hmax_pos : 0 < max 0.01 (a / (k * P.tau0)) := by
 108    apply lt_max_of_lt_left
 109    norm_num

papers checked against this theorem

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