kernel_match_pointwise

formal source

  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
  83  have hxpos : 0 < y + s := add_pos_of_pos_of_nonneg hy_pos (Real.sqrt_nonneg _)
  84  have hxinv :
  85      (y + s) ⁻¹ = y - s := by
  86    have hxnonzero : y + s ≠ 0 := ne_of_gt hxpos
  87    have hx' := congrArg (fun t => (y + s)⁻¹ * t) hxmul
  88    have hx'' : (y - s) = (y + s)⁻¹ := by
  89      simpa [mul_assoc, hxnonzero] using hx'
  90    simpa [recognitionProfile, y, s] using hx''.symm
  91  have hxsum : (y + s) + (y - s) = 2 * y := by ring