Theorem: DiracSeq.nonneg (ForML/Dirac.lean)

State before:
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ DiracSeq b x
Tactic:
simp [DiracSeq]
State after:
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ b / sqrt π * rexp (-(b * x) ^ 2)

State before:
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ b / sqrt π * rexp (-(b * x) ^ 2)
Tactic:
refine mul_nonneg ?_ ?_
State after:
case refine_1
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ b / sqrt π

case refine_2
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ rexp (-(b * x) ^ 2)

State before:
case refine_1
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ b / sqrt π

case refine_2
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ rexp (-(b * x) ^ 2)
Tactic:
. exact div_nonneg hb (sqrt_nonneg π)
State after:
case refine_2
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ rexp (-(b * x) ^ 2)

State before:
case refine_2
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ rexp (-(b * x) ^ 2)
Tactic:
. exact le_of_lt (exp_pos _)
State after:
no goals

State before:
case refine_1
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ b / sqrt π
Tactic:
exact div_nonneg hb (sqrt_nonneg π)
State after:
no goals

State before:
case refine_2
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ rexp (-(b * x) ^ 2)
Tactic:
exact le_of_lt (exp_pos _)
State after:
no goals