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

State before:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in (fun u => k * u) '' s, DiracSeq 1 x
Tactic:
rw [@integral_image_eq_integral_abs_deriv_smul _ _ _ _ _ (fun _ => k : ℝ → ℝ) hs]
State after:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| • DiracSeq 1 (k * x)

case hf'
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∀ x ∈ s, HasDerivWithinAt (fun u => k * u) k s x

case hf
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ Set.InjOn (fun u => k * u) s

State before:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| • DiracSeq 1 (k * x)

case hf'
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∀ x ∈ s, HasDerivWithinAt (fun u => k * u) k s x

case hf
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ Set.InjOn (fun u => k * u) s
Tactic:
rotate_left
State after:
case hf'
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∀ x ∈ s, HasDerivWithinAt (fun u => k * u) k s x

case hf
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ Set.InjOn (fun u => k * u) s

k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| • DiracSeq 1 (k * x)

State before:
case hf'
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∀ x ∈ s, HasDerivWithinAt (fun u => k * u) k s x

case hf
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ Set.InjOn (fun u => k * u) s

k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| • DiracSeq 1 (k * x)
Tactic:
. intro x _
  simp [mul_comm k]
  exact HasDerivAt.hasDerivWithinAt (hasDerivAt_mul_const k)
State after:
case hf
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ Set.InjOn (fun u => k * u) s

k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| • DiracSeq 1 (k * x)

State before:
case hf
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ Set.InjOn (fun u => k * u) s

k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| • DiracSeq 1 (k * x)
Tactic:
. apply Function.Injective.injOn
  simp [Function.Injective]
  intro u v
  intro h
  cases h with
  | inl h => exact h
  | inr h => exfalso; exact hk.ne' h
State after:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| • DiracSeq 1 (k * x)

State before:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| • DiracSeq 1 (k * x)
Tactic:
simp
State after:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| * DiracSeq 1 (k * x)

State before:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| * DiracSeq 1 (k * x)
Tactic:
rw [abs_of_pos hk]
State after:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, k * DiracSeq 1 (k * x)

State before:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, k * DiracSeq 1 (k * x)
Tactic:
simp [DiracSeq]
State after:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, k / sqrt π * rexp (-(k * x) ^ 2) = ∫ (x : ℝ) in s, k * ((sqrt π)⁻¹ * rexp (-(k * x) ^ 2))

State before:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, k / sqrt π * rexp (-(k * x) ^ 2) = ∫ (x : ℝ) in s, k * ((sqrt π)⁻¹ * rexp (-(k * x) ^ 2))
Tactic:
simp [← mul_assoc]
State after:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, k / sqrt π * rexp (-(k * x) ^ 2) = ∫ (x : ℝ) in s, k * (sqrt π)⁻¹ * rexp (-(k * x) ^ 2)

State before:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, k / sqrt π * rexp (-(k * x) ^ 2) = ∫ (x : ℝ) in s, k * (sqrt π)⁻¹ * rexp (-(k * x) ^ 2)
Tactic:
rfl
State after:
no goals

State before:
case hf'
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∀ x ∈ s, HasDerivWithinAt (fun u => k * u) k s x
Tactic:
intro x _
State after:
case hf'
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
x : ℝ
a✝ : x ∈ s
⊢ HasDerivWithinAt (fun u => k * u) k s x

State before:
case hf'
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
x : ℝ
a✝ : x ∈ s
⊢ HasDerivWithinAt (fun u => k * u) k s x
Tactic:
simp [mul_comm k]
State after:
case hf'
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
x : ℝ
a✝ : x ∈ s
⊢ HasDerivWithinAt (fun u => u * k) k s x

State before:
case hf'
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
x : ℝ
a✝ : x ∈ s
⊢ HasDerivWithinAt (fun u => u * k) k s x
Tactic:
exact HasDerivAt.hasDerivWithinAt (hasDerivAt_mul_const k)
State after:
no goals

State before:
case hf
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ Set.InjOn (fun u => k * u) s
Tactic:
apply Function.Injective.injOn
State after:
case hf.h
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ Function.Injective fun u => k * u

State before:
case hf.h
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ Function.Injective fun u => k * u
Tactic:
simp [Function.Injective]
State after:
case hf.h
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∀ ⦃a₁ a₂ : ℝ⦄, a₁ = a₂ ∨ k = 0 → a₁ = a₂

State before:
case hf.h
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∀ ⦃a₁ a₂ : ℝ⦄, a₁ = a₂ ∨ k = 0 → a₁ = a₂
Tactic:
intro u v
State after:
case hf.h
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
u v : ℝ
⊢ u = v ∨ k = 0 → u = v

State before:
case hf.h
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
u v : ℝ
⊢ u = v ∨ k = 0 → u = v
Tactic:
intro h
State after:
case hf.h
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
u v : ℝ
h : u = v ∨ k = 0
⊢ u = v

State before:
case hf.h
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
u v : ℝ
h : u = v ∨ k = 0
⊢ u = v
Tactic:
cases h with
| inl h => exact h
| inr h => exfalso; exact hk.ne' h
State after:
no goals

State before:
case hf.h.inl
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
u v : ℝ
h : u = v
⊢ u = v
Tactic:
exact h
State after:
no goals

State before:
case hf.h.inr
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
u v : ℝ
h : k = 0
⊢ u = v
Tactic:
exfalso
State after:
case hf.h.inr
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
u v : ℝ
h : k = 0
⊢ False

State before:
case hf.h.inr
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
u v : ℝ
h : k = 0
⊢ False
Tactic:
exact hk.ne' h
State after:
no goals