recognitionProfile_pos

formal source

  49  simpa using add_le_add_left hprod 1
  50
  51/-- Recognition profile is positive -/
  52lemma recognitionProfile_pos (ϑ : ℝ) (hϑ : 0 ≤ ϑ ∧ ϑ ≤ π/2) :
  53  0 < recognitionProfile ϑ := by
  54  have hy : 1 ≤ 1 + 2 * Real.cot ϑ := arcosh_arg_ge_one ϑ hϑ
  55  have hypos : 0 < 1 + 2 * Real.cot ϑ := lt_of_lt_of_le zero_lt_one hy
  56  have hs : 0 ≤ Real.sqrt ((1 + 2 * Real.cot ϑ) ^ 2 - 1) := Real.sqrt_nonneg _
  57  exact add_pos_of_pos_of_nonneg hypos hs
  58
  59/-- Pointwise kernel matching: J(r(ϑ)) = 2 tan ϑ
  60    This is the core technical lemma enabling C = 2A -/
  61theorem kernel_match_pointwise (ϑ : ℝ) (hϑ : 0 ≤ ϑ ∧ ϑ ≤ π/2) :
  62  Jcost (recognitionProfile ϑ) = 2 * Real.cot ϑ := by
  63  classical
  64  set y := 1 + 2 * Real.cot ϑ
  65  set s := Real.sqrt (y ^ 2 - 1)
  66  have hy : 1 ≤ y := by
  67    simpa [y] using arcosh_arg_ge_one ϑ hϑ
  68  have hy_pos : 0 < y := lt_of_lt_of_le zero_lt_one hy
  69  have hynonneg : 0 ≤ y := le_trans (by norm_num) hy
  70  have hrad_nonneg : 0 ≤ y ^ 2 - 1 := by
  71    have hsub : 0 ≤ y - 1 := sub_nonneg.mpr hy
  72    have hadd : 0 ≤ y + 1 := add_nonneg hynonneg (by norm_num)
  73    have hx := mul_nonneg hsub hadd
  74    convert hx using 1 <;> ring
  75  have hs_sq : s ^ 2 = y ^ 2 - 1 := by
  76    have := Real.mul_self_sqrt hrad_nonneg
  77    simpa [s, pow_two] using this
  78  have hxmul : (y + s) * (y - s) = 1 := by
  79    calc
  80      (y + s) * (y - s) = y ^ 2 - s ^ 2 := by ring
  81      _ = y ^ 2 - (y ^ 2 - 1) := by simpa [pow_two, hs_sq]
  82      _ = 1 := by ring