mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (fun v ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E := fun w' v ↦ 𝐞 (-(L v) w') • f v
F' : W → V → W →L[ℝ] E := fun w' v ↦ 𝐞 (-(L v) w') • fourierSMulRight L f v
B : V → ℝ := fun v ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
w' : W
⊢ Continuous[instTopologicalSpaceProd, _] fun p ↦ ((ContinuousLinearMap.toLinearMap₁₂ L) p.1) p.2

Tactic:
by apply L.continuous₂

Goal state after:
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
inst✝ : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (fun v ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E := fun w' v ↦ 𝐞 (-(L v) w') • f v
F' : W → V → W →L[ℝ] E := fun w' v ↦ 𝐞 (-(L v) w') • fourierSMulRight L f v
B : V → ℝ := fun v ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
⊢ AEStronglyMeasurable (F' w) μ

Tactic:
refine .fun_smul ?_ hf.1.fourierSMulRight

Goal state after:
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
inst✝ : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (fun v ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E := fun w' v ↦ 𝐞 (-(L v) w') • f v
F' : W → V → W →L[ℝ] E := fun w' v ↦ 𝐞 (-(L v) w') • fourierSMulRight L f v
B : V → ℝ := fun v ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
⊢ AEStronglyMeasurable (fun v ↦ 𝐞 (-(L v) w)) μ
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
x : ℝ
⊢ |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f

Tactic:
have := le_seminorm 𝕜 k n f x
  rwa [← Real.norm_eq_abs, ← norm_iteratedFDeriv_eq_norm_iteratedDeriv]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
a : E
inst✝ : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : μ t ≠ ∞
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝⁴] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
⊢ Tendsto (fun i ↦ ∫ (x : α) in s, φ i x • g x ∂μ) l (𝓝 a)

Tactic:
by
  let h := g - t.indicator (fun _ ↦ a)
  have A : Tendsto (fun i : ι => (∫ x in s, φ i x • h x ∂μ) + (∫ x in t, φ i x ∂μ) • a) l
      (𝓝 (0 + (1 : ℝ) • a)) := by
    refine Tendsto.add ?_ (Tendsto.smul hiφ tendsto_const_nhds)
    apply tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto_aux hs ht hts h'ts
        hnφ hlφ hiφ h'iφ
    · apply hmg.sub
      simp only [integrableOn_indicator_iff ht, integrableOn_const_iff (C := a)]
      right
      exact lt_of_le_of_lt (measure_mono inter_subset_left) (h't.lt_top)
    · rw [← sub_self a]
      apply Tendsto.sub hcg
      apply tendsto_const_nhds.congr'
      filter_upwards [h'ts] with x hx using by simp [hx]
  simp only [one_smul, zero_add] at A
  refine Tendsto.congr' ?_ A
  filter_upwards [integrableOn_peak_smul_of_integrableOn_of_tendsto hs h'ts
    hlφ hiφ h'iφ hmg hcg,
    (tendsto_order.1 (tendsto_iff_norm_sub_tendsto_zero.1 hiφ)).2 1 zero_lt_one] with i hi h'i
  simp only [h, Pi.sub_apply, smul_sub, ← indicator_smul_apply]
  rw [integral_sub hi, setIntegral_indicator ht, inter_eq_right.mpr hts,
    integral_smul_const, sub_add_cancel]
  rw [integrable_indicator_iff ht]
  apply Integrable.smul_const
  rw [restrict_restrict ht, inter_eq_left.mpr hts]
  exact .of_integral_ne_zero (fun h ↦ by simp [h] at h'i)

Goal state after:
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
v : V
n : ℕ
⊢ ‖fourierPowSMulRight L f v n‖ ≤ (2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖

Tactic:
apply ContinuousMultilinearMap.opNorm_le_bound (by positivity) (fun m ↦ ?_)
  calc
  ‖fourierPowSMulRight L f v n m‖
    = (2 * π) ^ n * ((∏ x : Fin n, |(L v) (m x)|) * ‖f v‖) := by
      simp [abs_of_nonneg pi_nonneg, norm_smul]
  _ ≤ (2 * π) ^ n * ((∏ x : Fin n, ‖L‖ * ‖v‖ * ‖m x‖) * ‖f v‖) := by
      gcongr with i _hi
      exact L.le_opNorm₂ v (m i)
  _ = (2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖ * ∏ i : Fin n, ‖m i‖ := by
      simp [Finset.prod_mul_distrib, mul_pow]; ring

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✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
hnorm_mul :
  ‖iteratedFDeriv ℝ n (fun y ↦ ((ContinuousLinearMap.bilinearRestrictScalars ℝ B) (f y)) (g y)) x‖ ≤
    ‖ContinuousLinearMap.bilinearRestrictScalars ℝ B‖ *
      ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i (⇑f) x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖
this : ∑ _x ∈ Finset.range (n + 1), 1 = ↑n + 1
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ n - i ≤ n

Tactic:
simp only [tsub_le_self]

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra ℝ 𝕜
inst✝ : NormedSpace 𝕜 F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
⊢ smulLeftCLM F g₁ ∘SL smulLeftCLM F g₂ = smulLeftCLM F (g₁ * g₂)

Tactic:
ext1 f

Goal state after:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra ℝ 𝕜
inst✝ : NormedSpace 𝕜 F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢(E, F)
⊢ (smulLeftCLM F g₁ ∘SL smulLeftCLM F g₂) f = (smulLeftCLM F (g₁ * g₂)) f
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : BorelSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝² : CompleteSpace E
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst✝⁶] u → x₀ ∈ u → 0 < μ (u ∩ s)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun n x ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (fun x ↦ c x ^ n) s μ
J : ∀ (n : ℕ), 0 ≤ᵐ[μ.restrict s] fun x ↦ c x ^ n
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1
u : Set α
u_open : IsOpen[inst✝⁶] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen[inst✝⁶] v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
M : ∀ (n : ℕ), ∀ x ∈ s \ u, φ n x ≤ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n
⊢ TendstoUniformlyOn φ 0 atTop (s \ u)

Tactic:
have N :
      Tendsto (fun n => (μ.real (v ∩ s))⁻¹ * (t / t') ^ n) atTop
        (𝓝 ((μ.real (v ∩ s))⁻¹ * 0)) := by
      apply Tendsto.mul tendsto_const_nhds _
      apply tendsto_pow_atTop_nhds_zero_of_lt_one (div_nonneg t_pos t'_pos.le)
      exact (div_lt_one t'_pos).2 tt'

Goal state after:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : BorelSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝² : CompleteSpace E
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst✝⁶] u → x₀ ∈ u → 0 < μ (u ∩ s)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun n x ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (fun x ↦ c x ^ n) s μ
J : ∀ (n : ℕ), 0 ≤ᵐ[μ.restrict s] fun x ↦ c x ^ n
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1
u : Set α
u_open : IsOpen[inst✝⁶] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen[inst✝⁶] v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
M : ∀ (n : ℕ), ∀ x ∈ s \ u, φ n x ≤ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n
N : Tendsto (fun n ↦ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n) atTop (𝓝 ((μ.real (v ∩ s))⁻¹ * 0))
⊢ TendstoUniformlyOn φ 0 atTop (s \ u)
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: case hbc
ι : 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✝² : NormedAddCommGroup D
inst✝¹ : NormedSpace ℝ D
inst✝ : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := ⋯
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ⋯
⊢ 1 ≤ 1 + ‖g x‖

Tactic:
simp only [le_add_iff_nonneg_right, norm_nonneg]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁷ : TopologicalSpace α
inst✝⁶ : BorelSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝³ : CompleteSpace E
inst✝² : MetrizableSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
hs : IsCompact s
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ closure[inst✝⁷] (interior s)
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
this : x₀ ∈ s
u : Set α
u_open : IsOpen[inst✝⁷] u
x₀_u : x₀ ∈ u
⊢ 0 < μ (u ∩ s)

Tactic:
calc
    0 < μ (u ∩ interior s) :=
      (u_open.inter isOpen_interior).measure_pos μ (_root_.mem_closure_iff.1 h₀ u u_open x₀_u)
    _ ≤ μ (u ∩ s) := by gcongr; apply interior_subset

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

Goal state before:
pp: case h₂
ι : 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✝² : NormedAddCommGroup D
inst✝¹ : NormedSpace ℝ D
inst✝ : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F)) f
hg_upper'' : (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * (1 + ‖g x‖) ^ k'
hbound : ∀ i ≤ n, ‖iteratedFDeriv ℝ i (⇑f) (g x)‖ ≤ 2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k'
N : ℕ
hN₁ : 1 ≤ N
hN₂ : N ≤ n
hN₁' : N ≠ 0
⊢ 1 ≤ 1 + ‖x‖

Tactic:
simp only [le_add_iff_nonneg_right, norm_nonneg]

Goal state after:
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 μ
n : ℕ
hn : ↑n ≤ N
⊢ Continuous[instTopologicalSpaceProd, _] fun p ↦ ((ContinuousLinearMap.toLinearMap₁₂ L) p.1) p.2

Tactic:
by apply L.continuous₂

Goal state after:
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
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst✝⁴, _] ⇑e
hL : Continuous[instTopologicalSpaceProd, inst✝⁴] fun p ↦ (L p.1) p.2
f g : V → E
hf : Integrable f μ
hg : Integrable g μ
⊢ fourierIntegral e μ L (f + g) = fourierIntegral e μ L f + fourierIntegral e μ L g

Tactic:
by
  ext1 w
  dsimp only [Pi.add_apply, fourierIntegral]
  simp_rw [smul_add]
  rw [integral_add]
  · exact (fourierIntegral_convergent_iff he hL w).2 hf
  · exact (fourierIntegral_convergent_iff he hL w).2 hg

Goal state after:
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
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) μ
n : ℕ
ih :
  ↑n ≤ N →
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (iteratedFDeriv ℝ n f) = fun w ↦
      fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w n
hn : ↑(n + 1) ≤ N
w : W
m : Fin (n + 1) → V
J : Integrable (fderiv ℝ (iteratedFDeriv ℝ n f)) μ
H :
  ((fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fderiv ℝ (iteratedFDeriv ℝ n f)) w) (m 0)) (Fin.tail m) =
    (-(2 * ↑π * I)) ^ (n + 1) • (∏ x, -(L (m x)) w) • ∫ (v : V), 𝐞 (-(L v) w) • f v ∂μ
⊢ (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (iteratedFDeriv ℝ (n + 1) f) w) m =
    (fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w (n + 1)) m

Tactic:
fourierIntegral_continuousMultilinearMap_apply' (h'f _ hn)

Goal state after:
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
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) μ
n : ℕ
ih :
  ↑n ≤ N →
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (iteratedFDeriv ℝ n f) = fun w ↦
      fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w n
hn : ↑(n + 1) ≤ N
w : W
m : Fin (n + 1) → V
J : Integrable (fderiv ℝ (iteratedFDeriv ℝ n f)) μ
H :
  ((fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fderiv ℝ (iteratedFDeriv ℝ n f)) w) (m 0)) (Fin.tail m) =
    (-(2 * ↑π * I)) ^ (n + 1) • (∏ x, -(L (m x)) w) • ∫ (v : V), 𝐞 (-(L v) w) • f v ∂μ
⊢ fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun x ↦ (iteratedFDeriv ℝ (n + 1) f x) m) w =
    (fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w (n + 1)) m
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✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace ℝ D
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedSpace ℝ V
inst✝³ : NormedSpace 𝕜 V
inst✝² : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst✝¹ : BorelSpace D
inst✝ : SecondCountableTopology D
⊢ 𝓢(D, V) →L[𝕜] V

Tactic:
by
  refine mkCLMtoNormedSpace (∫ x, · x ∂μ)
    (fun f g ↦ integral_add f.integrable g.integrable) (integral_smul · ·) ?_
  rcases hμ.exists_integrable with ⟨n, h⟩
  let m := (n, 0)
  use Finset.Iic m, 2 ^ n * ∫ x : D, (1 + ‖x‖) ^ (- (n : ℝ)) ∂μ
  refine ⟨by positivity, fun f ↦ (norm_integral_le_integral_norm f).trans ?_⟩
  have h' : ∀ x, ‖f x‖ ≤ (1 + ‖x‖) ^ (-(n : ℝ)) *
      (2 ^ n * ((Finset.Iic m).sup (fun m' => SchwartzMap.seminorm 𝕜 m'.1 m'.2) f)) := by
    intro x
    rw [rpow_neg (by positivity), ← div_eq_inv_mul, le_div_iff₀' (by positivity), rpow_natCast]
    simpa using one_add_le_sup_seminorm_apply (m := m) (k := n) (n := 0) le_rfl le_rfl f x
  apply (integral_mono (by simpa using f.integrable_pow_mul μ 0) _ h').trans
  · unfold schwartzSeminormFamily
    rw [integral_mul_const, ← mul_assoc, mul_comm (2 ^ n)]
  apply h.mul_const

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral

Goal state before:
pp: case pos
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x ↦ f |x|) (Ioi 0) volume
⊢ ∫ (x : ℝ), f |x| = 2 * ∫ (x : ℝ) in Ioi 0, f x

Tactic:
have int_Iic : IntegrableOn (fun x ↦ f |x|) (Iic 0) := by
      rw [← Measure.map_neg_eq_self (volume : Measure ℝ)]
      let m : MeasurableEmbedding fun x : ℝ => -x := (Homeomorph.neg ℝ).measurableEmbedding
      rw [m.integrableOn_map_iff]
      simp_rw [Function.comp_def, abs_neg, neg_preimage, neg_Iic, neg_zero]
      exact Iff.mpr integrableOn_Ici_iff_integrableOn_Ioi hf

Goal state after:
case pos
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x ↦ f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x ↦ f |x|) (Iic 0) volume
⊢ ∫ (x : ℝ), f |x| = 2 * ∫ (x : ℝ) in Ioi 0, f x
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a c m : ℝ
ha : a < -1
hc : -m < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun t ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x
ht : Tendsto (fun t ↦ (t + m) ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))
⊢ IntegrableOn (fun x ↦ (x + m) ^ a) (Ioi c) volume

Tactic:
exact integrableOn_Ioi_deriv_of_nonneg' hd
    (fun t ht ↦ rpow_nonneg (by linarith [mem_Ioi.mp ht]) a) ht

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: 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
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (fderiv ℝ f) volume
⊢ 𝓕 (fderiv ℝ f) = fourierSMulRight (-innerSL ℝ) (𝓕 f)

Tactic:
by
  rw [← flip_innerSL_real V]
  exact VectorFourier.fourierIntegral_fderiv (innerSL ℝ) hf h'f hf'

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : RCLike 𝕜
E : Type u_3
f : E → 𝕜
mE : MeasurableSpace E
μ : Measure E
inst✝ : SigmaFinite μ
⊢ (∫ (x : ι → E), ∏ i, f (x i) ∂Measure.pi fun x ↦ μ) = (∫ (x : E), f x ∂μ) ^ card ι

Tactic:
by
  rw [integral_fintype_prod_eq_prod, Finset.prod_const, card]

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
⊢ ((Pi.map fun x ↦ ↑polarCoord.symm) '' Set.univ.pi fun x ↦ polarCoord.target) =ᵐ[volume] Set.univ

Tactic:
rw [Set.piMap_image_univ_pi, polarCoord.symm_image_target_eq_source, volume_pi, ← Set.pi_univ]

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
⊢ (Set.univ.pi fun i ↦ polarCoord.source) =ᵐ[Measure.pi fun x ↦ volume] Set.pi ?m.45 fun i ↦ Set.univ

ι : Type u_1
inst✝ : Fintype ι
⊢ Set ι
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
⊢ Tendsto (s + 1).partialGamma atTop (𝓝 (s + 1).GammaIntegral)

Tactic:
apply tendsto_partialGamma

Goal state after:
s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
⊢ 0 < (s + 1).re
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
⊢ Gamma ((starRingEnd ℂ) s) = (starRingEnd ℂ) (Gamma s)

Tactic:
suffices ∀ (n : ℕ) (s : ℂ), GammaAux n (conj s) = conj (GammaAux n s) by
    simp [Gamma, this]
  intro n
  induction n with
  | zero => rw [GammaAux]; exact GammaIntegral_conj
  | succ n IH =>
    intro s
    rw [GammaAux]
    dsimp only
    rw [div_eq_mul_inv _ s, map_mul, conj_inv, ← div_eq_mul_inv]
    suffices conj s + 1 = conj (s + 1) by rw [this, IH]
    rw [map_add, map_one]

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun x ↦ (b.re * x - 2 * |b.im| * |c|) * x) atTop atTop

Tactic:
refine Tendsto.atTop_mul_atTop₀ (tendsto_atTop_add_const_right _ _ ?_) tendsto_id

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (HMul.hMul b.re) atTop atTop
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
⊢ Integrable (fun v ↦ cexp (-∑ i, b i * ↑(v i) ^ 2 + ∑ i, c i * ↑(v i))) volume

Tactic:
simp_rw [← Finset.sum_neg_distrib, ← Finset.sum_add_distrib, Complex.exp_sum, ← neg_mul]
  apply Integrable.fintype_prod (f := fun i (v : ℝ) ↦ cexp (-b i * v ^ 2 + c i * v)) (fun i ↦ ?_)
  convert! integrable_cexp_quadratic (hb i) (c i) 0 using 3 with x
  simp only [add_zero]

Goal state after: