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

kernel_match_differential

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)

 105theorem kernel_match_differential (ϑ : ℝ) (hϑ : 0 ≤ ϑ ∧ ϑ ≤ π/2) :
 106  Jcost (recognitionProfile ϑ) = 2 * Real.cot ϑ :=

proof body

Term-mode proof.

 107  kernel_match_pointwise ϑ hϑ
 108
 109/-- The integrand match: ∫ J(r(ϑ)) dϑ = 2 ∫ tan ϑ dϑ -/

depends on (2)

Lean names referenced from this declaration's body.