pith. machine review for the scientific record. sign in
lemma proved term proof

recognitionProfile_pos

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  52lemma recognitionProfile_pos (ϑ : ℝ) (hϑ : 0 ≤ ϑ ∧ ϑ ≤ π/2) :
  53  0 < recognitionProfile ϑ := by

proof body

Term-mode proof.

  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 -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (11)

Lean names referenced from this declaration's body.