thetaMin

formal source

  46def A_of_theta (θ : ℝ) : ℝ := -Real.log (Real.sin θ)
  47
  48/-- For budget `Amax > 0`, the minimal admissible angle. -/
  49def thetaMin (Amax : ℝ) : ℝ := Real.arcsin (Real.exp (-Amax))
  50
  51/-! ## Core limit and threshold lemmas (via classical results) -/
  52
  53open Filter
  54
  55/-- As θ → 0⁺, the kernel action `A_of_theta θ = -log(sin θ)` diverges to `+∞`. -/
  56theorem action_small_angle_diverges :
  57  Tendsto (fun θ => A_of_theta θ) (nhdsWithin 0 (Set.Ioi 0)) atTop := by
  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. -/
  62theorem theta_min_spec {Amax θ : ℝ}
  63    (hA : 0 < Amax) (hθ0 : 0 < θ) (hθh : θ ≤ π/2)
  64    (hAineq : A_of_theta θ ≤ Amax) :
  65    θ ≥ thetaMin Amax := by
  66  simpa [A_of_theta, thetaMin] using
  67    IndisputableMonolith.Cost.ClassicalResults.theta_min_spec_inequality Amax θ hA hθ0 hθh hAineq
  68
  69/-- Threshold is strictly positive and ≤ π/2 for any `Amax>0`. -/
  70theorem theta_min_range {Amax : ℝ} (hA : 0 < Amax) :
  71    0 < thetaMin Amax ∧ thetaMin Amax ≤ π/2 := by
  72  simpa [thetaMin] using
  73    IndisputableMonolith.Cost.ClassicalResults.theta_min_range Amax hA
  74
  75/-- If the angle is below the budget threshold, the action exceeds the budget. -/
  76theorem infeasible_below_thetaMin {Amax θ : ℝ}
  77    (hA : 0 < Amax) (hθ0 : 0 < θ) (hθh : θ ≤ π/2)
  78    (hθlt : θ < thetaMin Amax) :
  79    A_of_theta θ > Amax := by