mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case inr.inl
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k n : ℕ
hk : ↑k ≤ K
hn✝ : ↑n ≤ N
hn : n ≠ 0
Z :
  ‖0‖ ^ n * (‖0‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) 0‖) ≤
    ‖0‖ ^ n *
      ((2 * (π * ‖innerSL ℝ‖)) ^ k *
        ((2 * ↑k + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))
⊢ ‖0‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) 0‖ ≤
    (2 * π) ^ k * (2 * ↑k + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖

pp: case inr.inr
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k n : ℕ
hk : ↑k ≤ K
hn✝ : ↑n ≤ N
w : V
Z :
  ‖w‖ ^ n * (‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤
    ‖w‖ ^ n *
      ((2 * (π * ‖innerSL ℝ‖)) ^ k *
        ((2 * ↑k + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))
hn : n ≠ 0
hw : w ≠ 0
⊢ ‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤
    (2 * π) ^ k * (2 * ↑k + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖

Tactic:
·

Goal state after:
case inr.inl
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k n : ℕ
hk : ↑k ≤ K
hn✝ : ↑n ≤ N
hn : n ≠ 0
Z :
  ‖0‖ ^ n * (‖0‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) 0‖) ≤
    ‖0‖ ^ n *
      ((2 * (π * ‖innerSL ℝ‖)) ^ k *
        ((2 * ↑k + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))
⊢ ‖0‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) 0‖ ≤
    (2 * π) ^ k * (2 * ↑k + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case refine_1
s x : ℝ
hx : rexp (-(1 / 2) * x) = 0
⊢ rexp (-x) * x ^ s = 0

pp: case refine_2
s : ℝ
⊢ Tendsto (fun x ↦ rexp (-x) * x ^ s / rexp (-(1 / 2) * x)) atTop (𝓝 0)

Tactic:
·

Goal state after:
case refine_1
s x : ℝ
hx : rexp (-(1 / 2) * x) = 0
⊢ rexp (-x) * x ^ s = 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case left
s : ℝ
h : 0 < s
⊢ IntegrableOn (fun x ↦ rexp (-x) * x ^ (s - 1)) (Ioc 0 1) volume

pp: case right
s : ℝ
h : 0 < s
⊢ IntegrableOn (fun x ↦ rexp (-x) * x ^ (s - 1)) (Ioi 1) volume

Tactic:
·

Goal state after:
case left
s : ℝ
h : 0 < s
⊢ IntegrableOn (fun x ↦ rexp (-x) * x ^ (s - 1)) (Ioc 0 1) volume
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case right
s : ℝ
h : 0 < s
⊢ IntegrableOn (fun x ↦ rexp (-x) * x ^ (s - 1)) (Ioi 1) volume

Tactic:
·

Goal state after:
case right
s : ℝ
h : 0 < s
⊢ IntegrableOn (fun x ↦ rexp (-x) * x ^ (s - 1)) (Ioi 1) volume
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case left
s : ℂ
hs : 0 < s.re
⊢ AEStronglyMeasurable (fun x ↦ ↑(rexp (-x)) * ↑x ^ (s - 1)) (volume.restrict (Ioi 0))

pp: case right
s : ℂ
hs : 0 < s.re
⊢ HasFiniteIntegral (fun x ↦ ↑(rexp (-x)) * ↑x ^ (s - 1)) (volume.restrict (Ioi 0))

Tactic:
·

Goal state after:
case left
s : ℂ
hs : 0 < s.re
⊢ AEStronglyMeasurable (fun x ↦ ↑(rexp (-x)) * ↑x ^ (s - 1)) (volume.restrict (Ioi 0))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case right
s : ℂ
hs : 0 < s.re
⊢ HasFiniteIntegral (fun x ↦ ↑(rexp (-x)) * ↑x ^ (s - 1)) (volume.restrict (Ioi 0))

Tactic:
·

Goal state after:
case right
s : ℂ
hs : 0 < s.re
⊢ HasFiniteIntegral (fun x ↦ ↑(rexp (-x)) * ↑x ^ (s - 1)) (volume.restrict (Ioi 0))
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case left
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}
⊢ 0 < x ^ 2 + y ^ 2

pp: case right
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}
⊢ 0 ≤ (Complex.equivRealProd.symm (x, y)).re ∨ (Complex.equivRealProd.symm (x, y)).im ≠ 0

Tactic:
·

Goal state after:
case left
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}
⊢ 0 < x ^ 2 + y ^ 2
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case left.inl
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.1}
⊢ 0 < x ^ 2 + y ^ 2

pp: case left.inr
x y : ℝ
hxy : (x, y) ∈ {q | q.2 ≠ 0}
⊢ 0 < x ^ 2 + y ^ 2

Tactic:
·

Goal state after:
case left.inl
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.1}
⊢ 0 < x ^ 2 + y ^ 2
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case left.inl
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.1}
⊢ 0 < x ^ 2 + y ^ 2

Tactic:
dsimp at hxy

Goal state after:
case left.inl
x y : ℝ
hxy : 0 < x
⊢ 0 < x ^ 2 + y ^ 2
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case left.inr
x y : ℝ
hxy : (x, y) ∈ {q | q.2 ≠ 0}
⊢ 0 < x ^ 2 + y ^ 2

Tactic:
·

Goal state after:
case left.inr
x y : ℝ
hxy : (x, y) ∈ {q | q.2 ≠ 0}
⊢ 0 < x ^ 2 + y ^ 2
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case right
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}
⊢ 0 ≤ (Complex.equivRealProd.symm (x, y)).re ∨ (Complex.equivRealProd.symm (x, y)).im ≠ 0

Tactic:
·

Goal state after:
case right
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}
⊢ 0 ≤ (Complex.equivRealProd.symm (x, y)).re ∨ (Complex.equivRealProd.symm (x, y)).im ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case right.inl
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.1}
⊢ 0 ≤ (Complex.equivRealProd.symm (x, y)).re ∨ (Complex.equivRealProd.symm (x, y)).im ≠ 0

pp: case right.inr
x y : ℝ
hxy : (x, y) ∈ {q | q.2 ≠ 0}
⊢ 0 ≤ (Complex.equivRealProd.symm (x, y)).re ∨ (Complex.equivRealProd.symm (x, y)).im ≠ 0

Tactic:
·

Goal state after:
case right.inl
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.1}
⊢ 0 ≤ (Complex.equivRealProd.symm (x, y)).re ∨ (Complex.equivRealProd.symm (x, y)).im ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case right.inr
x y : ℝ
hxy : (x, y) ∈ {q | q.2 ≠ 0}
⊢ 0 ≤ (Complex.equivRealProd.symm (x, y)).re ∨ (Complex.equivRealProd.symm (x, y)).im ≠ 0

Tactic:
·

Goal state after:
case right.inr
x y : ℝ
hxy : (x, y) ∈ {q | q.2 ≠ 0}
⊢ 0 ≤ (Complex.equivRealProd.symm (x, y)).re ∨ (Complex.equivRealProd.symm (x, y)).im ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x✝ : ℝ
⊢ -(↑(rexp (-x✝)) * ↑x✝ ^ s) = (-fun x ↦ ↑(rexp (-x)) * ↑x ^ (s + 1 - 1)) x✝

pp: s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
⊢ 0 < (s + 1).re

Tactic:
·

Goal state after:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x✝ : ℝ
⊢ -(↑(rexp (-x✝)) * ↑x✝ ^ s) = (-fun x ↦ ↑(rexp (-x)) * ↑x ^ (s + 1 - 1)) x✝
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x✝ : ℝ
⊢ -(↑(rexp (-x✝)) * ↑x✝ ^ s) = (-fun x ↦ ↑(rexp (-x)) * ↑x ^ (s + 1 - 1)) x✝

pp: s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
⊢ 0 < (s + 1).re

Tactic:
· simp only [ofReal_exp, ofReal_neg, add_sub_cancel_right]; rfl

Goal state after:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
⊢ 0 < (s + 1).re
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
⊢ 0 < (s + 1).re

Tactic:
·

Goal state after:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
⊢ 0 < (s + 1).re
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case inl
r : ℝ
hr : r ∈ Ioi 0
hθ : 0 ∈ Ioo (-π) π
⊢ ((r, 0).1 * cos (r, 0).2, (r, 0).1 * sin (r, 0).2) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}

pp: case inr
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
h'θ : θ ≠ 0
⊢ ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}

Tactic:
·

Goal state after:
case inl
r : ℝ
hr : r ∈ Ioi 0
hθ : 0 ∈ Ioo (-π) π
⊢ ((r, 0).1 * cos (r, 0).2, (r, 0).1 * sin (r, 0).2) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case left
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ AEStronglyMeasurable (fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))) (volume.restrict (Ioc 0 Y))

pp: case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ HasFiniteIntegral (fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))) (volume.restrict (Ioc 0 Y))

Tactic:
·

Goal state after:
case left
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ AEStronglyMeasurable (fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))) (volume.restrict (Ioc 0 Y))
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case inr
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
h'θ : θ ≠ 0
⊢ ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}

Tactic:
·

Goal state after:
case inr
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
h'θ : θ ≠ 0
⊢ ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case fst
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ √((r * cos θ) ^ 2 + (r * sin θ) ^ 2) = r

pp: case snd
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ (Complex.equivRealProd.symm (r * cos θ, r * sin θ)).arg = θ

Tactic:
·

Goal state after:
case fst
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ √((r * cos θ) ^ 2 + (r * sin θ) ^ 2) = r
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc 0 Y → rexp (-x) * x ^ (s.re - 1) = ‖↑(rexp (-x))‖ * ‖↑x ^ (s - 1)‖

pp: case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ MeasurableSet (Ioc 0 Y)

Tactic:
·

Goal state after:
case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc 0 Y → rexp (-x) * x ^ (s.re - 1) = ‖↑(rexp (-x))‖ * ‖↑x ^ (s - 1)‖
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case snd
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ (Complex.equivRealProd.symm (r * cos θ, r * sin θ)).arg = θ

Tactic:
·

Goal state after:
case snd
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ (Complex.equivRealProd.symm (r * cos θ, r * sin θ)).arg = θ
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ MeasurableSet (Ioc 0 Y)

Tactic:
·

Goal state after:
case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ MeasurableSet (Ioc 0 Y)
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case refine_1
A : MapsTo (⇑Complex.equivRealProd.symm) ({q | 0 < q.1} ∪ {q | q.2 ≠ 0}) Complex.slitPlane
z : ℂ
hz : z ∈ Complex.slitPlane
⊢ ContinuousWithinAt Complex.arg Complex.slitPlane z

pp: case refine_2
A : MapsTo (⇑Complex.equivRealProd.symm) ({q | 0 < q.1} ∪ {q | q.2 ≠ 0}) Complex.slitPlane
⊢ ContinuousOn (⇑Complex.equivRealProd.symm) ({q | 0 < q.1} ∪ {q | q.2 ≠ 0})

Tactic:
·

Goal state after:
case refine_1
A : MapsTo (⇑Complex.equivRealProd.symm) ({q | 0 < q.1} ∪ {q | q.2 ≠ 0}) Complex.slitPlane
z : ℂ
hz : z ∈ Complex.slitPlane
⊢ ContinuousWithinAt Complex.arg Complex.slitPlane z
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case refine_2
A : MapsTo (⇑Complex.equivRealProd.symm) ({q | 0 < q.1} ∪ {q | q.2 ≠ 0}) Complex.slitPlane
⊢ ContinuousOn (⇑Complex.equivRealProd.symm) ({q | 0 < q.1} ∪ {q | q.2 ≠ 0})

Tactic:
·

Goal state after:
case refine_2
A : MapsTo (⇑Complex.equivRealProd.symm) ({q | 0 < q.1} ∪ {q | q.2 ≠ 0}) Complex.slitPlane
⊢ ContinuousOn (⇑Complex.equivRealProd.symm) ({q | 0 < q.1} ∪ {q | q.2 ≠ 0})
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case refine_2
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
hx : x ∈ Ioo 0 X
d1 : HasDerivAt (fun y ↦ rexp (-y)) (-rexp (-x)) x
t : HasDerivAt (fun x ↦ id x ^ s) (s * id ↑x ^ (s - 1) * 1) ↑x
⊢ HasDerivAt (fun y ↦ ↑y ^ s) (s * ↑x ^ (s - 1)) x

pp: case refine_1
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
hx : x ∈ Ioo 0 X
d1 : HasDerivAt (fun y ↦ rexp (-y)) (-rexp (-x)) x
⊢ id ↑x ∈ slitPlane

Tactic:
·

Goal state after:
case refine_2
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
hx : x ∈ Ioo 0 X
d1 : HasDerivAt (fun y ↦ rexp (-y)) (-rexp (-x)) x
t : HasDerivAt (fun x ↦ id x ^ s) (s * id ↑x ^ (s - 1) * 1) ↑x
⊢ HasDerivAt (fun y ↦ ↑y ^ s) (s * ↑x ^ (s - 1)) x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case refine_1
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
hx : x ∈ Ioo 0 X
d1 : HasDerivAt (fun y ↦ rexp (-y)) (-rexp (-x)) x
⊢ id ↑x ∈ slitPlane

Tactic:
·

Goal state after:
case refine_1
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
hx : x ∈ Ioo 0 X
d1 : HasDerivAt (fun y ↦ rexp (-y)) (-rexp (-x)) x
⊢ id ↑x ∈ slitPlane
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case hf
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ AEStronglyMeasurable (fun x ↦ (-x) ^ s * rexp (-b * x ^ 2)) (volume.restrict (Ioi 0))

pp: case h
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioi 0), ‖(-a) ^ s * rexp (-b * a ^ 2)‖ ≤ a ^ s * rexp (-b * a ^ 2)

Tactic:
·

Goal state after:
case hf
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ AEStronglyMeasurable (fun x ↦ (-x) ^ s * rexp (-b * x ^ 2)) (volume.restrict (Ioi 0))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case h
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioi 0), ‖(-a) ^ s * rexp (-b * a ^ 2)‖ ≤ a ^ s * rexp (-b * a ^ 2)

Tactic:
·

Goal state after:
case h
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioi 0), ‖(-a) ^ s * rexp (-b * a ^ 2)‖ ≤ a ^ s * rexp (-b * a ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case refine_1
b : ℂ
hb : 0 < b.re
⊢ Continuous fun x ↦ -b * ↑x ^ 2

pp: case refine_2
b : ℂ
hb : 0 < b.re
⊢ HasFiniteIntegral (fun x ↦ ↑x * cexp (-b * ↑x ^ 2)) volume

Tactic:
·

Goal state after:
case refine_1
b : ℂ
hb : 0 < b.re
⊢ Continuous fun x ↦ -b * ↑x ^ 2
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] (f : (i : Fin n) → E i → 𝕜),
    ∫ (x : (i : Fin n) → E i), ∏ i, f i (x i) ∂Measure.pi μ = ∏ i, ∫ (x : E i), f i x ∂μ i
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
⊢ ∫ (x : (i : Fin (n + 1)) → E i), ∏ i, f i (x i) ∂Measure.pi μ =
    ∫ (x : E 0 × ((i : Fin n) → E i.succ)), f 0 x.1 * ∏ i, f i.succ (x.2 i) ∂(μ 0).prod (Measure.pi fun i ↦ μ i.succ)

Tactic:
by
          rw [← ((measurePreserving_piFinSuccAbove μ 0).symm).integral_comp']
          simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNthEquiv,
            Fin.prod_univ_succ, Fin.insertNth_zero, Equiv.coe_fn_mk, Fin.cons_succ,
            Fin.zero_succAbove, cast_eq, Fin.cons_zero]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: f : ℝ × ℝ → ℝ≥0∞
⊢ ∫⁻ (x : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |(fderivPolarCoordSymm x).det| * f (↑polarCoord.symm x) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f (↑polarCoord.symm p)

pp: case hf
f : ℝ × ℝ → ℝ≥0∞
⊢ InjOn (↑polarCoord.symm) polarCoord.target

pp: f : ℝ × ℝ → ℝ≥0∞
⊢ MeasurableSet polarCoord.target

Tactic:
·

Goal state after:
f : ℝ × ℝ → ℝ≥0∞
⊢ ∫⁻ (x : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |(fderivPolarCoordSymm x).det| * f (↑polarCoord.symm x) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f (↑polarCoord.symm p)
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: case hφ
ι : Type u_2
inst✝³ : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
f : X i → E
hf : AEStronglyMeasurable f (μ i)
⊢ AEMeasurable (Function.eval i) (Measure.pi μ)

pp: case hfm
ι : Type u_2
inst✝³ : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
f : X i → E
hf : AEStronglyMeasurable f (μ i)
⊢ AEStronglyMeasurable f (map (Function.eval i) (Measure.pi μ))

Tactic:
·

Goal state after:
case hφ
ι : Type u_2
inst✝³ : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
f : X i → E
hf : AEStronglyMeasurable f (μ i)
⊢ AEMeasurable (Function.eval i) (Measure.pi μ)
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: case hfm
ι : Type u_2
inst✝³ : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
f : X i → E
hf : AEStronglyMeasurable f (μ i)
⊢ AEStronglyMeasurable f (map (Function.eval i) (Measure.pi μ))

Tactic:
·

Goal state after:
case hfm
ι : Type u_2
inst✝³ : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
f : X i → E
hf : AEStronglyMeasurable f (μ i)
⊢ AEStronglyMeasurable f (map (Function.eval i) (Measure.pi μ))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case inl
b : ℝ
hb : b ≤ 0
⊢ ∫ (x : ℝ), rexp (-b * x ^ 2) = √(π / b)

pp: case inr
b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ), rexp (-b * x ^ 2) = √(π / b)

Tactic:
·

Goal state after:
case inl
b : ℝ
hb : b ≤ 0
⊢ ∫ (x : ℝ), rexp (-b * x ^ 2) = √(π / b)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case inl
b : ℝ
hb : b ≤ 0
⊢ π / b ≤ 0

pp: case inl
b : ℝ
hb : b ≤ 0
⊢ ¬Integrable (fun x ↦ rexp (-b * x ^ 2)) volume

Tactic:
·

Goal state after:
case inl
b : ℝ
hb : b ≤ 0
⊢ π / b ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case inl
b : ℝ
hb : b ≤ 0
⊢ ¬Integrable (fun x ↦ rexp (-b * x ^ 2)) volume

Tactic:
·

Goal state after:
case inl
b : ℝ
hb : b ≤ 0
⊢ ¬Integrable (fun x ↦ rexp (-b * x ^ 2)) volume
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case inr
b : ℝ
hb : 0 < b
⊢ (∫ (x : ℝ), ↑(rexp (-b * x ^ 2))) ^ 2 = ↑(π / b)

Tactic:
← RCLike.algebraMap_eq_ofReal,

Goal state after:
case inr
b : ℝ
hb : 0 < b
⊢ (∫ (x : ℝ), (algebraMap ℝ ℂ) (rexp (-b * x ^ 2))) ^ 2 = (algebraMap ℝ ℂ) (π / b)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case zero
s : ℂ
h1 : -s.re < ↑0
⊢ GammaAux 0 s = GammaAux (0 + 1) s

pp: case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑(n + 1)
⊢ GammaAux (n + 1) s = GammaAux (n + 1 + 1) s

Tactic:
·

Goal state after:
case zero
s : ℂ
h1 : -s.re < ↑0
⊢ GammaAux 0 s = GammaAux (0 + 1) s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑(n + 1)
⊢ GammaAux (n + 1) s = GammaAux (n + 1 + 1) s

Tactic:
·

Goal state after:
case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑(n + 1)
⊢ GammaAux (n + 1) s = GammaAux (n + 1 + 1) s
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: case hbc
b : ℂ
hb : 0 < b.re
c✝ T✝ : ℝ
hT✝ : 0 ≤ T✝
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
⊢ 2 * b.im * y ≤ 2 * |b.im| * |c|

pp: case hbc
b : ℂ
hb : 0 < b.re
c✝ T✝ : ℝ
hT✝ : 0 ≤ T✝
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
⊢ y ^ 2 ≤ c ^ 2

Tactic:
·

Goal state after:
case hbc
b : ℂ
hb : 0 < b.re
c✝ T✝ : ℝ
hT✝ : 0 ≤ T✝
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
⊢ 2 * b.im * y ≤ 2 * |b.im| * |c|
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
⊢ ∀ᵐ (a : V), Tendsto (fun n ↦ cexp (-↑n⁻¹ * ↑‖a‖ ^ 2) • f a) atTop (𝓝 (f a))

pp: V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
⊢ ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (fun a ↦ cexp (-↑n⁻¹ * ↑‖a‖ ^ 2) • f a) volume

pp: V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
⊢ ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : V), ‖cexp (-↑n⁻¹ * ↑‖a‖ ^ 2) • f a‖ ≤ ‖f a‖

Tactic:
·

Goal state after:
V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
⊢ ∀ᵐ (a : V), Tendsto (fun n ↦ cexp (-↑n⁻¹ * ↑‖a‖ ^ 2) • f a) atTop (𝓝 (f a))
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
⊢ ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (fun a ↦ cexp (-↑n⁻¹ * ↑‖a‖ ^ 2) • f a) volume

pp: V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
⊢ ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : V), ‖cexp (-↑n⁻¹ * ↑‖a‖ ^ 2) • f a‖ ≤ ‖f a‖

Tactic:
·

Goal state after:
V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
⊢ ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (fun a ↦ cexp (-↑n⁻¹ * ↑‖a‖ ^ 2) • f a) volume
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: case hbc
b : ℂ
hb : 0 < b.re
c✝ T✝ : ℝ
hT✝ : 0 ≤ T✝
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
⊢ y ^ 2 ≤ c ^ 2

Tactic:
·

Goal state after:
case hbc
b : ℂ
hb : 0 < b.re
c✝ T✝ : ℝ
hT✝ : 0 ≤ T✝
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
⊢ y ^ 2 ≤ c ^ 2