theorem proved term proof

`action_small_angle_diverges`

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

formal statement (Lean)

  56theorem action_small_angle_diverges :
  57  Tendsto (fun θ => A_of_theta θ) (nhdsWithin 0 (Set.Ioi 0)) atTop := by

proof body

Term-mode proof.

  58  simpa [A_of_theta] using
  59    IndisputableMonolith.Cost.ClassicalResults.neg_log_sin_tendsto_atTop_at_zero_right
  60
  61/-- Budget inequality implies the minimal angle threshold. -/

depends on (3)

Lean names referenced from this declaration's body.

neg_log_sin_tendsto_atTop_at_zero_right in IndisputableMonolith.Cost.ClassicalResults decl_use
A_of_theta in IndisputableMonolith.Measurement.RecognitionAngle.ActionSmallAngle decl_use
Cost in IndisputableMonolith.Measurement.RSNative.Core decl_use