def
definition
def or abbrev
NegativeControl
show as:
view Lean formalization →
formal statement (Lean)
156def NegativeControl := ℝ → Prop
proof body
Definition body.
157
158/-- Velocity permutation: randomly reassign v_obs to different radii. -/