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

Goal state before:
pp: case e'_6
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp f 2 (volume.restrict (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
⊢ (b - a)⁻¹ • ∫ (x : ℝ) in a..b, ‖f x‖ ^ 2 =
    ∫ (t : AddCircle (b - a)), ‖↑↑(MemLp.toLp (liftIoc (b - a) a f) h) t‖ ^ 2 ∂haarAddCircle

Tactic:
· nth_rw 2 [← add_sub_cancel a b]
    rw [← AddCircle.integral_liftIoc_eq_intervalIntegral, ← Function.comp_def (f := (‖·‖ ^ 2))]
    simp only [liftIoc_comp_apply, ← AddCircle.integral_haarAddCircle]
    apply integral_congr_ae
    filter_upwards [h.coeFn_toLp] with x hx
    simp [hx]

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 t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
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₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball 0 δ
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn (fun x ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ 2 * δ
⊢ ∫ (x : α) in s \ u, δ * ‖g x‖ ∂μ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ

Tactic:
by
        rw [integral_const_mul]
        apply mul_le_mul_of_nonneg_left (setIntegral_mono_set hmg.norm _ _) δpos.le
        · filter_upwards with x using norm_nonneg _
        · filter_upwards using sdiff_subset (s := s) (t := u)

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 t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
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₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball 0 δ
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn (fun x ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ 2 * δ
C : ‖∫ (x : α) in s \ u, φ i x • g x ∂μ‖ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ
⊢ ‖∫ (x : α) in s, φ i x • g x ∂μ‖ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ

Tactic:
calc
    ‖∫ x in s, φ i x • g x ∂μ‖ =
      ‖(∫ x in s \ u, φ i x • g x ∂μ) + ∫ x in s ∩ u, φ i x • g x ∂μ‖ := by
      conv_lhs => rw [← sdiff_union_inter s u]
      rw [setIntegral_union disjoint_sdiff_inter (hs.inter u_open.measurableSet)
          (h''i.mono_set sdiff_subset) (h''i.mono_set inter_subset_left)]
    _ ≤ ‖∫ x in s \ u, φ i x • g x ∂μ‖ + ‖∫ x in s ∩ u, φ i x • g x ∂μ‖ := norm_add_le _ _
    _ ≤ (δ * ∫ x in s, ‖g x‖ ∂μ) + 2 * δ := add_le_add C B

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✝¹⁰ : NormedField 𝕜
inst✝⁹ : NormedField 𝕜'
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace 𝕜' G
inst✝¹ : SMulCommClass ℝ 𝕜' G
σ : 𝕜 →+* 𝕜'
inst✝ : RingHomIsometric σ
A : 𝓢(D, E) → G
hadd : ∀ (f g : 𝓢(D, E)), A (f + g) = A f + A g
hsmul : ∀ (a : 𝕜) (f : 𝓢(D, E)), A (a • f) = σ a • A f
hbound : ∃ s C, 0 ≤ C ∧ ∀ (f : 𝓢(D, E)), ‖A f‖ ≤ C * (s.sup (schwartzSeminormFamily 𝕜 D E)) f
f : 𝓢(D, E) →ₛₗ[σ] G := { toFun := fun x ↦ A x, map_add' := hadd, map_smul' := hsmul }
⊢ Continuous ⇑{ toFun := fun x ↦ A x, map_add' := hadd, map_smul' := hsmul }

Tactic:
apply WithSeminorms.continuous_normedSpace_rng G (schwartz_withSeminorms 𝕜 D E)

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✝¹⁰ : NormedField 𝕜
inst✝⁹ : NormedField 𝕜'
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace 𝕜' G
inst✝¹ : SMulCommClass ℝ 𝕜' G
σ : 𝕜 →+* 𝕜'
inst✝ : RingHomIsometric σ
A : 𝓢(D, E) → G
hadd : ∀ (f g : 𝓢(D, E)), A (f + g) = A f + A g
hsmul : ∀ (a : 𝕜) (f : 𝓢(D, E)), A (a • f) = σ a • A f
hbound : ∃ s C, 0 ≤ C ∧ ∀ (f : 𝓢(D, E)), ‖A f‖ ≤ C * (s.sup (schwartzSeminormFamily 𝕜 D E)) f
f : 𝓢(D, E) →ₛₗ[σ] G := ⋯
⊢ ∃ s C,
    (normSeminorm 𝕜' G).comp { toFun := fun x ↦ A x, map_add' := hadd, map_smul' := hsmul } ≤
      C • s.sup (schwartzSeminormFamily 𝕜 D E)
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case hbc
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
K : ℕ∞ω
C : ℝ
hf : ContDiff ℝ K f
n k : ℕ
hk : ↑k ≤ K
v : V
hv : ∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C
T : (W →L[ℝ] ℝ) [×n]→L[ℝ] W [×n]→L[ℝ] ℝ := ⋯
I₁ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m ⇑T fun x ↦ L v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m)
I₂ :
  ∀ (m : ℕ),
    ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x ↦ L)) v‖ ≤
      ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m
I₃ :
  ∀ (m : ℕ),
    ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x ↦ L)) v‖ ≤ ↑(n.descFactorial m) * ‖L‖ ^ n * ‖v‖ ^ (n - m)
A : ContDiff ℝ K fun y ↦ T fun x ↦ L y
⊢ ∑ i ∈ Finset.range (k + 1),
      ↑(k.choose i) * ‖iteratedFDeriv ℝ i (fun y ↦ T fun x ↦ L y) v‖ * ‖iteratedFDeriv ℝ (k - i) f v‖ ≤
    (2 * ↑n + 2) ^ k * (‖L‖ ^ n * C)

Tactic:
calc
  ∑ i ∈ Finset.range (k + 1),
    k.choose i * ‖iteratedFDeriv ℝ i (fun (y : V) ↦ T (fun _ ↦ L y)) v‖ *
      ‖iteratedFDeriv ℝ (k - i) f v‖
    ≤ ∑ i ∈ Finset.range (k + 1),
      k.choose i * (n.descFactorial i * ‖L‖ ^ n * ‖v‖ ^ (n - i)) *
        ‖iteratedFDeriv ℝ (k - i) f v‖ := by
    gcongr with i _hi
    exact I₃ i
  _ = ∑ i ∈ Finset.range (k + 1), (k.choose i * n.descFactorial i * ‖L‖ ^ n) *
        (‖v‖ ^ (n - i) * ‖iteratedFDeriv ℝ (k - i) f v‖) := by
    congr with i
    ring
  _ ≤ ∑ i ∈ Finset.range (k + 1), (k.choose i * (n + 1 : ℕ) ^ k * ‖L‖ ^ n) * C := by
    gcongr with i hi
    · norm_cast
      calc n.descFactorial i ≤ n ^ i := Nat.descFactorial_le_pow _ _
      _ ≤ (n + 1) ^ i := by gcongr; lia
      _ ≤ (n + 1) ^ k := by gcongr; exacts [le_add_self, Finset.mem_range_succ_iff.mp hi]
    · exact hv _ (by lia) _ (by lia)
  _ = (2 * n + 2) ^ k * (‖L‖ ^ n * C) := by
    simp only [← Finset.sum_mul, ← Nat.cast_sum, Nat.sum_range_choose, mul_one, ← mul_assoc,
      Nat.cast_pow, Nat.cast_ofNat, Nat.cast_add, Nat.cast_one, ← mul_pow, mul_add]

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
⊢ μ (u ∩ interior s) ≤ μ (u ∩ s)

Tactic:
by gcongr; apply interior_subset

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 : ¬Integrable f μ
⊢ fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f = 0

Tactic:
ext w

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
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : ¬Integrable f μ
w : W
⊢ fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f w = 0 w
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : NormedSpace ℝ H
inst✝⁵ : FiniteDimensional ℝ H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℂ V
f g : 𝓢(H, V)
μ : Measure H
inst✝ : μ.HasTemperateGrowth
⊢ (fun a ↦ inner ℂ (↑↑(f.toLp 2 μ) a) (↑↑(g.toLp 2 μ) a)) =ᵐ[μ] fun a ↦ inner ℂ (f a) (g a)

Tactic:
have hf_ae := f.coeFn_toLp 2 μ

Goal state after:
H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : NormedSpace ℝ H
inst✝⁵ : FiniteDimensional ℝ H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℂ V
f g : 𝓢(H, V)
μ : Measure H
inst✝ : μ.HasTemperateGrowth
hf_ae : ↑↑(f.toLp 2 μ) =ᵐ[μ] ⇑f
⊢ (fun a ↦ inner ℂ (↑↑(f.toLp 2 μ) a) (↑↑(g.toLp 2 μ) a)) =ᵐ[μ] fun a ↦ inner ℂ (f a) (g a)
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: c : ℝ
⊢ IntegrableOn rexp (Iic c) volume

Tactic:
by
  refine
    integrableOn_Iic_of_intervalIntegral_norm_bounded (exp c) c
      (fun y => intervalIntegrable_exp.1) tendsto_id
      (eventually_of_mem (Iic_mem_atBot 0) fun y _ => ?_)
  simp_rw [norm_of_nonneg (exp_pos _).le, integral_exp, sub_le_self_iff]
  exact (exp_pos _).le

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
V : Type u_5
W : Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : NormedSpace 𝕜 V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → F →L[ℝ] E
a : F
w : W
he : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑e
hf : Integrable f μ
⊢ (fourierIntegral e μ (ContinuousLinearMap.toLinearMap₁₂ L) f w) a =
    fourierIntegral e μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun x ↦ (f x) a) w

Tactic:
rw [fourierIntegral, ContinuousLinearMap.integral_apply]

Goal state after:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
V : Type u_5
W : Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : NormedSpace 𝕜 V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → F →L[ℝ] E
a : F
w : W
he : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑e
hf : Integrable f μ
⊢ ∫ (x : V), (e (-((ContinuousLinearMap.toLinearMap₁₂ L) x) w) • f x) a ∂μ =
    fourierIntegral e μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun x ↦ (f x) a) w

case φ_int
𝕜 : Type u_1
E : Type u_3
F : Type u_4
V : Type u_5
W : Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : NormedSpace 𝕜 V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → F →L[ℝ] E
a : F
w : W
he : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑e
hf : Integrable f μ
⊢ Integrable (fun v ↦ e (-((ContinuousLinearMap.toLinearMap₁₂ L) v) w) • f v) μ
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (fun x ↦ ‖↑x ^ s‖) (Ioi t) volume
⊢ s.re < -1

Tactic:
refine (integrableOn_Ioi_rpow_iff ht).mp <| h.congr_fun (fun a ha ↦ ?_) measurableSet_Ioi

Goal state after:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (fun x ↦ ‖↑x ^ s‖) (Ioi t) volume
a : ℝ
ha : a ∈ Ioi t
⊢ (fun x ↦ ‖↑x ^ s‖) a = a ^ s.re
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
W : Type u_2
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : InnerProductSpace ℝ W
inst✝³ : MeasurableSpace W
inst✝² : BorelSpace W
inst✝¹ : FiniteDimensional ℝ W
inst✝ : FiniteDimensional ℝ V
c : ℂ
f : ↥(Lp E 1 volume)
x : V
⊢ (fourierTransform (c • f)) x = ((RingHom.id ℂ) c • fourierTransform f) x

Tactic:
simp only [Lp.fourierTransform_apply, BoundedContinuousFunction.coe_smul, Real.fourier_eq]

Goal state after:
V : Type u_1
W : Type u_2
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : InnerProductSpace ℝ W
inst✝³ : MeasurableSpace W
inst✝² : BorelSpace W
inst✝¹ : FiniteDimensional ℝ W
inst✝ : FiniteDimensional ℝ V
c : ℂ
f : ↥(Lp E 1 volume)
x : V
⊢ ∫ (v : V), 𝐞 (-⟪v, x⟫) • ↑↑(c • f) v = (RingHom.id ℂ) c • ∫ (v : V), 𝐞 (-⟪v, x⟫) • ↑↑f v
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case e'_2
x : ℝ
hx : x ∈ Ioi 0
this : (x ^ 2) ^ (1 / 2 - 1) = x⁻¹
⊢ (2 * x ^ (2 - 1)) • (rexp (-x ^ 2) * (x ^ 2) ^ (1 / 2 - 1)) = 2 * rexp (-1 * x ^ 2)

Tactic:
rw [smul_eq_mul, this]

Goal state after:
case e'_2
x : ℝ
hx : x ∈ Ioi 0
this : (x ^ 2) ^ (1 / 2 - 1) = x⁻¹
⊢ 2 * x ^ (2 - 1) * (rexp (-x ^ 2) * x⁻¹) = 2 * rexp (-1 * x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
⊢ ∫ (v : ℝ), cexp (↑(-2 * π * v * t) * I + -↑π * b * ↑v ^ 2 + 2 * ↑π * c * ↑v) =
    1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)

Tactic:
have (x : ℝ) : ↑(-2 * π * x * t) * I + -π * b * x ^ 2 + 2 * π * c * x =
    -π * b * x ^ 2 + (-2 * π * I * t + 2 * π * c) * x + 0 := by push_cast; ring

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ ∫ (v : ℝ), cexp (↑(-2 * π * v * t) * I + -↑π * b * ↑v ^ 2 + 2 * ↑π * c * ↑v) =
    1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ι → ℂ
⊢ (↑π / b) ^ (↑Finset.univ.card * 2⁻¹) * cexp (∑ x, c x ^ 2 / (4 * b)) =
    (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp ((∑ i, c i ^ 2) / (4 * b))

Tactic:
Fintype.card,

Goal state after:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ι → ℂ
⊢ (↑π / b) ^ (↑Finset.univ.card * 2⁻¹) * cexp (∑ x, c x ^ 2 / (4 * b)) =
    (↑π / b) ^ (↑Finset.univ.card / 2) * cexp ((∑ i, c i ^ 2) / (4 * b))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: case e'_2.e'_7
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w v : V
⊢ cexp (-(2 * ↑π * ↑⟪w, v⟫ * I) + (-(b * ↑‖v‖ ^ 2) + 2 * ↑π * I * ↑⟪x, v⟫)) =
    cexp (-b * ↑‖v‖ ^ 2 + 2 * ↑π * I * ↑⟪x - w, v⟫)

pp: case e'_3
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w : V
⊢ -(↑π ^ 2 * ↑‖x - w‖ ^ 2) / b = (2 * ↑π * I) ^ 2 * ↑‖x - w‖ ^ 2 / (4 * b)

Tactic:
· congr 1
    simp [inner_sub_left]
    ring

Goal state after:
case e'_3
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w : V
⊢ -(↑π ^ 2 * ↑‖x - w‖ ^ 2) / b = (2 * ↑π * I) ^ 2 * ↑‖x - w‖ ^ 2 / (4 * b)
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
s : Set E
hf : IsVanishingOn (⇑f) s
g : E → ℂ
hg : Function.HasTemperateGrowth g
u : 𝓢(E, ℂ)
hu : tsupport ⇑u ⊆ s
⊢ tsupport ⇑((SchwartzMap.smulLeftCLM ℂ g) u) ⊆ s

Tactic:
SchwartzMap.smulLeftCLM_apply hg

Goal state after:
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
s : Set E
hf : IsVanishingOn (⇑f) s
g : E → ℂ
hg : Function.HasTemperateGrowth g
u : 𝓢(E, ℂ)
hu : tsupport ⇑u ⊆ s
⊢ (tsupport fun x ↦ g x • u x) ⊆ s
Module: Mathlib.Analysis.Distribution.TemperedDistribution

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℂ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul ℂ F
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
⊢ smulLeftCLM F g₂ ∘SL smulLeftCLM F g₁ = smulLeftCLM F (g₁ * g₂)

Tactic:
by
  ext1 f
  simp [hg₁, hg₂]

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
a✝ : UnitAddTorus d
⊢ ↑↑(mFourierLp 2 i) a✝ = (mFourier i) a✝ →
    (starRingEnd ℂ) (↑↑(mFourierLp 2 i) a✝) * ↑↑f a✝ = (mFourier (-i)) a✝ • ↑↑f a✝

Tactic:
ht

Goal state after:
d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
a✝ : UnitAddTorus d
ht : ↑↑(mFourierLp 2 i) a✝ = (mFourier i) a✝
⊢ (starRingEnd ℂ) (↑↑(mFourierLp 2 i) a✝) * ↑↑f a✝ = (mFourier (-i)) a✝ • ↑↑f a✝
Module: Mathlib.Analysis.Fourier.Convolution

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F₁
inst✝⁹ : NormedAddCommGroup F₂
inst✝⁸ : NormedAddCommGroup F₃
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : NormedSpace 𝕜 F₁
inst✝² : NormedSpace 𝕜 F₂
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℂ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : Integrable f₁ volume
hf₂ : Integrable f₂ volume
ξ : E
⊢ ∫ (y : E) (x : E), 𝐞 (-inner ℝ x ξ) • (B (f₁ (x - y))) (f₂ y) =
    ∫ (y : E) (x : E), 𝐞 (-inner ℝ (y + x) ξ) • (B (f₁ x)) (f₂ y)

Tactic:
congr
    ext y
    -- Linear change of variables
    convert! integral_sub_right_eq_self _ y (μ := volume)
    congr
    simp

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f : C(UnitAddTorus d, ℂ)
h : Summable (mFourierCoeff ⇑f)
sum_L2 : HasSum (fun i ↦ mFourierCoeff (⇑f) i • mFourierLp 2 i) ((ContinuousMap.toLp 2 volume ℂ) f)
⊢ Summable fun a ↦ ‖mFourierCoeff (⇑f) a • mFourier a‖

Tactic:
simpa only [norm_smul, mFourier_norm, mul_one] using h.norm

Goal state after:
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: k m n : ℕ+
⊢ (↑m).Coprime ↑k → (↑n).Coprime ↑k → (↑(m * n)).Coprime ↑k

Tactic:
rw [mul_coe]

Goal state after:
k m n : ℕ+
⊢ (↑m).Coprime ↑k → (↑n).Coprime ↑k → (↑m * ↑n).Coprime ↑k
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: k m n : ℕ+
⊢ (↑k).Coprime ↑m → (↑k).Coprime ↑n → (↑k).Coprime ↑(m * n)

Tactic:
rw [mul_coe]

Goal state after:
k m n : ℕ+
⊢ (↑k).Coprime ↑m → (↑k).Coprime ↑n → (↑k).Coprime (↑m * ↑n)
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∀ x ∈ n.primeFactors, 1 + f x = ↑(ζ x) + f x

Tactic:
intro p hp

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
p : ℕ
hp : p ∈ n.primeFactors
⊢ 1 + f p = ↑(ζ p) + f p
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
this : ∃ T, ∀ (w : V), T ≤ ‖w‖ → ‖∫ (v : V), 𝐞 (-⟪v, w⟫) • f v‖ < ε
⊢ ∃ a, ∀ (b : ℝ), a ≤ b → ∀ (a : V), ‖a‖ = b → ‖∫ (v : V), 𝐞 (-⟪v, a⟫) • f v‖ < ε

Tactic:
exact
      let ⟨T, hT⟩ := this
      ⟨T, fun b hb v hv => hT v (hv.symm ▸ hb)⟩

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∀ x ∈ n.primeFactors, 1 - f x = 1 + ((↑μ).pmul f) x

Tactic:
intro p hp

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
p : ℕ
hp : p ∈ n.primeFactors
⊢ 1 - f p = 1 + ((↑μ).pmul f) p
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
G : ℕ → R := fun n ↦ ∑ i ∈ n.divisors, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
⊢ ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
suffices ∑ d ∈ n.divisors, μ (n / d) • G d = f n by
      rw [sum_divisorsAntidiagonal' (f := fun x y => μ x • g y), ← this, sum_congr rfl]
      intro d hd
      rw [← h d (pos_of_mem_divisors hd) <| hs d n (dvd_of_mem_divisors hd) hnP]

Goal state after:
case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
G : ℕ → R := fun n ↦ ∑ i ∈ n.divisors, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
⊢ ∑ d ∈ n.divisors, μ (n / d) • G d = f n
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
ζ : M
hζ : IsPrimitiveRoot ζ n
⊢ Set.InjOn (fun x ↦ ζ ^ x) ↑(range n)

Tactic:
intro i hi j hj e

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
ζ : M
hζ : IsPrimitiveRoot ζ n
i : ℕ
hi : i ∈ ↑(range n)
j : ℕ
hj : j ∈ ↑(range n)
e : (fun x ↦ ζ ^ x) i = (fun x ↦ ζ ^ x) j
⊢ i = j