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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : CommRing 𝕜
V : Type u_2
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
inst✝⁴ : MeasurableSpace V
W : Type u_3
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f₁ f₂ : V → E
hf : f₁ =ᵐ[μ] f₂
⊢ fourierIntegral e μ L f₁ = fourierIntegral e μ L f₂

Tactic:
ext

Goal state after:
𝕜 : Type u_1
inst✝⁷ : CommRing 𝕜
V : Type u_2
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
inst✝⁴ : MeasurableSpace V
W : Type u_3
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f₁ f₂ : V → E
hf : f₁ =ᵐ[μ] f₂
x✝ : W
⊢ fourierIntegral e μ L f₁ x✝ = fourierIntegral e μ L f₂ x✝
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
⊢ HasFTaylorSeriesUpTo N (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) fun w n ↦
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun v ↦ fourierPowSMulRight L f v n) w

Tactic:
constructor

Goal state after:
case zero_eq
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
⊢ ∀ (x : W),
    (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun v ↦ fourierPowSMulRight L f v 0) x).curry0 =
      fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f x

case fderiv
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
⊢ ∀ (m : ℕ),
    ↑m < N →
      ∀ (x : W),
        HasFDerivAt
          (fun y ↦ fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun v ↦ fourierPowSMulRight L f v m) y)
          (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun v ↦ fourierPowSMulRight L f v m.succ)
              x).curryLeft
          x

case cont
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
⊢ ∀ (m : ℕ),
    ↑m ≤ N →
      Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun x ↦
        fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun v ↦ fourierPowSMulRight L f v m) x
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f✝ g✝ : 𝓢(E, F)
⊢ (f✝ + g✝).toBoundedContinuousFunction = f✝.toBoundedContinuousFunction + g✝.toBoundedContinuousFunction

Tactic:
ext

Goal state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f✝ g✝ : 𝓢(E, F)
x✝ : E
⊢ (f✝ + g✝).toBoundedContinuousFunction x✝ = (f✝.toBoundedContinuousFunction + g✝.toBoundedContinuousFunction) x✝
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
a✝ : 𝕜
f✝ : 𝓢(E, F)
⊢ (a✝ • f✝).toBoundedContinuousFunction = (RingHom.id 𝕜) a✝ • f✝.toBoundedContinuousFunction

Tactic:
ext

Goal state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
a✝ : 𝕜
f✝ : 𝓢(E, F)
x✝ : E
⊢ (a✝ • f✝).toBoundedContinuousFunction x✝ = ((RingHom.id 𝕜) a✝ • f✝.toBoundedContinuousFunction) x✝
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : ProperSpace E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f✝ g✝ : 𝓢(E, F)
⊢ (f✝ + g✝).toZeroAtInfty = f✝.toZeroAtInfty + g✝.toZeroAtInfty

Tactic:
ext

Goal state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : ProperSpace E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f✝ g✝ : 𝓢(E, F)
x✝ : E
⊢ (f✝ + g✝).toZeroAtInfty x✝ = (f✝.toZeroAtInfty + g✝.toZeroAtInfty) x✝
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : ProperSpace E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
a✝ : 𝕜
f✝ : 𝓢(E, F)
⊢ (a✝ • f✝).toZeroAtInfty = (RingHom.id 𝕜) a✝ • f✝.toZeroAtInfty

Tactic:
ext

Goal state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : ProperSpace E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
a✝ : 𝕜
f✝ : 𝓢(E, F)
x✝ : E
⊢ (a✝ • f✝).toZeroAtInfty x✝ = ((RingHom.id 𝕜) a✝ • f✝.toZeroAtInfty) x✝
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: case h₂
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
hk : eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) p μ < ∞
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ eLpNorm (fun x ↦ (1 + ‖x‖) ^ k • f x) ∞ μ ≤
    2 ^ k * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)

Tactic:
refine eLpNormEssSup_le_of_ae_nnnorm_bound (ae_of_all μ fun x ↦ ?_)

Goal state after:
case h₂
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
hk : eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) p μ < ∞
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
x : E
⊢ ‖(1 + ‖x‖) ^ k • f x‖₊ ≤ ↑2 ^ k * (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f).toNNReal
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: 𝕜 : Type u_1
inst✝²³ : CommRing 𝕜
V : Type u_2
inst✝²² : AddCommGroup V
inst✝²¹ : Module 𝕜 V
inst✝²⁰ : MeasurableSpace V
W : Type u_3
inst✝¹⁹ : AddCommGroup W
inst✝¹⁸ : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℂ E
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace ℂ F
inst✝¹³ : NormedAddCommGroup G
inst✝¹² : NormedSpace ℂ G
inst✝¹¹ : TopologicalSpace 𝕜
inst✝¹⁰ : IsTopologicalRing 𝕜
inst✝⁹ : TopologicalSpace V
inst✝⁸ : BorelSpace V
inst✝⁷ : TopologicalSpace W
inst✝⁶ : MeasurableSpace W
inst✝⁵ : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst✝⁴ : SigmaFinite μ
inst✝³ : SigmaFinite ν
inst✝² : SecondCountableTopologyEither W V
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : V → E
g : W → F
M : E →L[ℂ] F →L[ℂ] G
he : Continuous[inst✝¹¹, _] ⇑e
hL : Continuous[instTopologicalSpaceProd, inst✝¹¹] fun p ↦ (L p.1) p.2
hf : Integrable f μ
hg : Integrable g ν
⊢ ∫ (ξ : W), (M (fourierIntegral e μ L f ξ)) (g ξ) ∂ν = ∫ (x : V), (M (f x)) (fourierIntegral e ν L.flip g x) ∂μ

Tactic:
by
  by_cases hG : CompleteSpace G; swap; · simp [integral, hG]
  calc
  ∫ ξ, M.flip (g ξ) (∫ x, e (-L x ξ) • f x ∂μ) ∂ν
    = ∫ ξ, (∫ x, M.flip (g ξ) (e (-L x ξ) • f x) ∂μ) ∂ν := by
    congr with ξ
    apply (ContinuousLinearMap.integral_comp_comm _ _).symm
    exact (fourierIntegral_convergent_iff he hL _).2 hf
  _ = ∫ x, (∫ ξ, M.flip (g ξ) (e (-L x ξ) • f x) ∂ν) ∂μ :=
    integral_fourierIntegral_swap M.flip he hL hf hg
  _ = ∫ x, (∫ ξ, M (f x) (e (-L.flip ξ x) • g ξ) ∂ν) ∂μ := by
    simp only [ContinuousLinearMap.flip_apply, ContinuousLinearMap.map_smul_of_tower,
      smul_apply, LinearMap.flip_apply]
  _ = ∫ x, M (f x) (∫ ξ, e (-L.flip ξ x) • g ξ ∂ν) ∂μ := by
    congr with x
    apply ContinuousLinearMap.integral_comp_comm
    apply (fourierIntegral_convergent_iff he _ _).2 hg
    exact hL.comp continuous_swap

Goal state after:
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ ‖f.toLp ∞ μ‖ ≤ (SchwartzMap.seminorm ℝ 0 0) f

Tactic:
rw [norm_toLp, ← ENNReal.ofReal_le_ofReal_iff (by positivity),
    ENNReal.ofReal_toReal (memLp_top f μ).eLpNorm_ne_top]
  exact eLpNormEssSup_le_of_ae_bound <| .of_forall <| norm_le_seminorm ℝ f

Goal state after:
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : MeasurableSpace D
inst✝⁶ : MeasurableSpace E
inst✝⁵ : OpensMeasurableSpace E
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedSpace 𝕜 F
inst✝² : SMulCommClass ℝ 𝕜 F
inst✝¹ : SecondCountableTopologyEither E F
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ ∃ s C, 0 ≤ C ∧ ∀ (f : 𝓢(E, F)), ‖f.toLp p μ‖ ≤ C * (s.sup (schwartzSeminormFamily 𝕜 E F)) f

Tactic:
by
    rcases norm_toLp_le_seminorm 𝕜 F p μ with ⟨k, C, hC_pos, hC⟩
    exact ⟨Finset.Iic (k, 0), C, hC_pos, hC⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

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

Tactic:
constructor

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

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: s : ℂ
hs : 0 < s.re
⊢ IntegrableOn (fun x ↦ ↑(rexp (-x)) * ↑x ^ (s - 1)) (Ioi 0) volume

Tactic:
constructor

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

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: x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}
⊢ 0 < x ^ 2 + y ^ 2 ∧ (0 ≤ (Complex.equivRealProd.symm (x, y)).re ∨ (Complex.equivRealProd.symm (x, y)).im ≠ 0)

Tactic:
constructor

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

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.Gamma.Basic

Goal state before:
pp: 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))
⊢ IntegrableOn (fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))) (Ioc 0 Y) volume

Tactic:
constructor

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))

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))
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

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

Tactic:
ext

Goal state after:
case fst
r θ : ℝ
hr : (r, θ).1 ∈ Ioi 0
hθ : (r, θ).2 ∈ Ioo (-π) π
⊢ (√(((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).1 ^ 2 +
            ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).2 ^ 2),
        (Complex.equivRealProd.symm ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2)).arg).1 =
    (r, θ).1

case snd
r θ : ℝ
hr : (r, θ).1 ∈ Ioi 0
hθ : (r, θ).2 ∈ Ioo (-π) π
⊢ (√(((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).1 ^ 2 +
            ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2).2 ^ 2),
        (Complex.equivRealProd.symm ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2)).arg).2 =
    (r, θ).2
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

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

Tactic:
simpa using integrable_rpow_mul_exp_neg_mul_sq hb (by simp : (-1 : ℝ) < 0)

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
E : Fin 0 → Type u_3
mE : (i : Fin 0) → MeasurableSpace (E i)
μ : (i : Fin 0) → Measure (E i)
inst✝ : ∀ (i : Fin 0), SigmaFinite (μ i)
f : (i : Fin 0) → E i → 𝕜
⊢ ∫ (x : (i : Fin 0) → E i), ∏ i, f i (x i) ∂Measure.pi μ = ∏ i, ∫ (x : E i), f i x ∂μ i

Tactic:
simp [measureReal_def]

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

Goal state before:
pp: ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
⊢ (∫ (p : ι → ℝ × ℝ) in Set.univ.pi fun x ↦ polarCoord.target, (∏ i, (p i).1) • f fun i ↦ ↑polarCoord.symm (p i)) =
    ∫ (x : ι → ℝ × ℝ) in (Pi.map fun x ↦ ↑polarCoord.symm) '' Set.univ.pi fun x ↦ polarCoord.target, f x

Tactic:
convert!
    (integral_image_eq_integral_abs_det_fderiv_smul volume measurableSet_pi_polarCoord_target
        (fun p _ ↦ (hasFDerivAt_pi_polarCoord_symm p).hasFDerivWithinAt) injOn_pi_polarCoord_symm
        f).symm using 1

Goal state after:
case e'_2
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
⊢ (∫ (p : ι → ℝ × ℝ) in Set.univ.pi fun x ↦ polarCoord.target, (∏ i, (p i).1) • f fun i ↦ ↑polarCoord.symm (p i)) =
    ∫ (x : ι → ℝ × ℝ) in Set.univ.pi fun x ↦ polarCoord.target,
      |(fderivPiPolarCoordSymm x).det| • f fun i ↦ ↑polarCoord.symm (x i)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c T✝ : ℝ
hT : 0 ≤ T✝
T : ℝ
⊢ 0 ≤ T →
    ∀ {c y : ℝ},
      |y| ≤ |c| → ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))

Tactic:
hT

Goal state after:
b : ℂ
hb : 0 < b.re
c T✝ : ℝ
hT✝ : 0 ≤ T✝
T : ℝ
hT : 0 ≤ T
⊢ ∀ {c y : ℝ},
    |y| ≤ |c| → ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
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:
· filter_upwards with c using
      AEStronglyMeasurable.smul (Continuous.aestronglyMeasurable (by fun_prop)) hf.1

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, ∀ᵐ (a : V), ‖cexp (-↑n⁻¹ * ↑‖a‖ ^ 2) • f a‖ ≤ ‖f a‖
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)
⊢ 1 / ↑r * (1 / ↑r) ^ (a - 1) * ∫ (t : ℝ) in Ioi 0, ↑t ^ (a - 1) * cexp (-↑t) = (1 / ↑r) ^ a * Gamma a

Tactic:
by
      rw [aux, Gamma_eq_integral ha]
      congr 2 with x
      rw [ofReal_exp, ofReal_neg, mul_comm]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: case e'_3
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
⊢ c ^ 2 * ↑‖w‖ ^ 2 = ∑ i, (c * ↑(w.ofLp i)) ^ 2

Tactic:
simp only [EuclideanSpace.norm_eq, Real.norm_eq_abs, sq_abs, mul_pow, ← Finset.mul_sum]

Goal state after:
case e'_3
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
⊢ c ^ 2 * ↑√(∑ x, w.ofLp x ^ 2) ^ 2 = c ^ 2 * ∑ i, ↑(w.ofLp i) ^ 2
Module: Mathlib.Analysis.Distribution.FourierMultiplier

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : NormedSpace ℂ F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
c : ℂ
⊢ (fourierMultiplierCLM F fun x ↦ c) = c • ContinuousLinearMap.id ℂ 𝓢'(E, F)

Tactic:
ext

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : NormedSpace ℂ F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
c : ℂ
x✝¹ : 𝓢'(E, F)
x✝ : 𝓢(E, ℂ)
⊢ ((fourierMultiplierCLM F fun x ↦ c) x✝¹) x✝ = ((c • ContinuousLinearMap.id ℂ 𝓢'(E, F)) x✝¹) x✝
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : 𝓢(V, E)
m : V
⊢ (SchwartzMap.evalCLM ℝ V E m) (-(2 * ↑π * Complex.I) • (smulRightCLM ℂ E (innerSL ℝ)) f) =
    -(2 * ↑π * Complex.I) • (smulLeftCLM E fun x ↦ inner ℝ x m) f

Tactic:
ext

Goal state after:
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : 𝓢(V, E)
m x✝ : V
⊢ ((SchwartzMap.evalCLM ℝ V E m) (-(2 * ↑π * Complex.I) • (smulRightCLM ℂ E (innerSL ℝ)) f)) x✝ =
    (-(2 * ↑π * Complex.I) • (smulLeftCLM E fun x ↦ inner ℝ x m) f) x✝
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : 𝓢(V, E)
m : V
⊢ 𝓕 ((SchwartzMap.evalCLM ℝ V E m) ((fderivCLM ℝ V E) f)) =
    (2 * ↑π * Complex.I) • (smulLeftCLM E fun x ↦ inner ℝ x m) (𝓕 f)

Tactic:
ext

Goal state after:
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : 𝓢(V, E)
m x✝ : V
⊢ (𝓕 ((SchwartzMap.evalCLM ℝ V E m) ((fderivCLM ℝ V E) f))) x✝ =
    ((2 * ↑π * Complex.I) • (smulLeftCLM E fun x ↦ inner ℝ x m) (𝓕 f)) x✝
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
x : E
⊢ (1 + ‖x‖ ^ 2) ^ (s / 2) * (1 + ‖x‖ ^ 2) ^ (s' / 2) = (1 + ‖x‖ ^ 2) ^ (s / 2 + s' / 2)

Tactic:
by
      rw [← Real.rpow_add (by positivity)]

Goal state after:
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : NormedSpace ℂ F
s : ℝ
f g : 𝓢'(E, F)
⊢ (besselPotential E F (-s)) f = g ↔ (besselPotential E F s) g = f

Tactic:
constructor

Goal state after:
case mp
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : NormedSpace ℂ F
s : ℝ
f g : 𝓢'(E, F)
⊢ (besselPotential E F (-s)) f = g → (besselPotential E F s) g = f

case mpr
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : NormedSpace ℂ F
s : ℝ
f g : 𝓢'(E, F)
⊢ (besselPotential E F s) g = f → (besselPotential E F (-s)) f = g