`R3`

definition

show as: view math explainer →

module: IndisputableMonolith.Measurement.RecognitionAngle.BlindCone
domain: Measurement
line: 19 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Measurement.RecognitionAngle.BlindCone on GitHub at line 19.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  16namespace Measurement
  17namespace RecognitionAngle
  18
  19abbrev R3 := EuclideanSpace ℝ (Fin 3)
  20
  21/-- Budget-dependent minimal angle threshold. -/
  22@[simp] def θmin (Amax : ℝ) : ℝ := thetaMin Amax
  23
  24/-- The blind cone at `x` with budget `Amax`: pairs `(y,z)` whose separation angle at `x`
  25falls below `θmin(Amax)`. -/
  26def blindCone (x : R3) (Amax : ℝ) : Set (R3 × R3) :=
  27  { p | angleAt x p.1 p.2 < θmin Amax }
  28
  29/-- Existence of a strictly positive threshold angle for any `Amax>0`. -/
  30theorem blind_cone_exists {Amax : ℝ} (hA : 0 < Amax) : 0 < θmin Amax := by
  31  have h := theta_min_range (Amax := Amax) hA
  32  exact h.left
  33
  34/-- Upper bound: `θmin(Amax) ≤ π/2` for any `Amax>0`. Useful for cap-measure bounds. -/
  35theorem theta_min_le_pi_half {Amax : ℝ} (hA : 0 < Amax) : θmin Amax ≤ π/2 := by
  36  have h := theta_min_range (Amax := Amax) hA
  37  exact h.right
  38
  39end RecognitionAngle
  40end Measurement
  41end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.