mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.GramMatrix

Goal state before:
pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Finite n
v : n → E
h_gram : (gram 𝕜 v).PosDef
this : Fintype n
y : n → 𝕜
hy : ∑ i, y i • v i = 0
⊢ ∀ (i : n), y i = 0

Tactic:
have := h_gram.dotProduct_mulVec_pos (x := y)

Goal state after:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Finite n
v : n → E
h_gram : (gram 𝕜 v).PosDef
this✝ : Fintype n
y : n → 𝕜
hy : ∑ i, y i • v i = 0
this : y ≠ 0 → 0 < star y ⬝ᵥ gram 𝕜 v *ᵥ y
⊢ ∀ (i : n), y i = 0
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Algebra ℝ A
inst✝⁵ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : IsSelfAdjoint a
⊢ abs a = cfc (fun x ↦ ‖x‖) a

Tactic:
rw [abs_eq_cfcₙ_norm _, cfcₙ_eq_cfc]

Goal state after:
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
h_two : ENNReal.toReal 2 = 2
⊢ (∫⁻ (a : α), ‖↑↑f a‖ₑ ^ ENNReal.toReal 2 ∂μ) ^ (1 / ENNReal.toReal 2 * ↑2) = ∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ

Tactic:
one_div,

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
h_two : ENNReal.toReal 2 = 2
⊢ (∫⁻ (a : α), ‖↑↑f a‖ₑ ^ ENNReal.toReal 2 ∂μ) ^ ((ENNReal.toReal 2)⁻¹ * ↑2) = ∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ
Module: Mathlib.Geometry.Manifold.SmoothApprox

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
ε : E → ℝ
n : ℕ∞
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ε
ε_pos : ∀ (x : E), 0 < ε x
S U : Set E
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] S
hU : U ∈ 𝓝ˢ S
hfU : ContDiffOn ℝ (↑n) f U
g : C^↑n⟮𝓘(ℝ, E), E; 𝓘(ℝ, F), F⟯
g_approx : ∀ (x : E), dist (g x) (f x) < ε x
g_eqOn : EqOn (⇑g) f S
g_supp : support ⇑g ⊆ support f
⊢ ∃ g, ContDiff ℝ (↑n) g ∧ (∀ (x : E), dist (g x) (f x) < ε x) ∧ EqOn g f S ∧ support g ⊆ support f

Tactic:
exact ⟨g, g.contMDiff.contDiff, g_approx, g_eqOn, g_supp⟩

Goal state after:
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
x : α
⊢ ‖g x‖ = g x

Tactic:
Real.norm_eq_abs,

Goal state after:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
x : α
⊢ |g x| = g x
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α → E
g_support : HasCompactSupport g
g_cont : Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_mem : MemLp g (↑p.toNNReal) μ
hg : (∫ (a : α), ‖(f - g) a‖ ^ (ENNReal.ofReal p).toReal ∂μ) ^ (ENNReal.ofReal p).toReal⁻¹ ≤ ε ^ (1 / p)
⊢ ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε

Tactic:
one_div,

Goal state after:
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α → E
g_support : HasCompactSupport g
g_cont : Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_mem : MemLp g (↑p.toNNReal) μ
hg : (∫ (a : α), ‖(f - g) a‖ ^ (ENNReal.ofReal p).toReal ∂μ) ^ (ENNReal.ofReal p).toReal⁻¹ ≤ ε ^ p⁻¹
⊢ ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g,
    HasCompactSupport g ∧
      ∫⁻ (x : α), ‖f x - g x‖ₑ ∂μ ≤ ε ∧
        Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ Integrable g μ

Tactic:
by
  simp only [← memLp_one_iff_integrable, ← eLpNorm_one_eq_lintegral_enorm] at hf ⊢
  exact hf.exists_hasCompactSupport_eLpNorm_sub_le ENNReal.one_ne_top hε

Goal state after:
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α →ᵇ E
g_mem : MemLp (⇑g) (↑p.toNNReal) μ
hg : (∫ (a : α), ‖(f - ⇑g) a‖ ^ (ENNReal.ofReal p).toReal ∂μ) ^ (ENNReal.ofReal p).toReal⁻¹ ≤ ε ^ (1 / p)
⊢ ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε

Tactic:
one_div,

Goal state after:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α →ᵇ E
g_mem : MemLp (⇑g) (↑p.toNNReal) μ
hg : (∫ (a : α), ‖(f - ⇑g) a‖ ^ (ENNReal.ofReal p).toReal ∂μ) ^ (ENNReal.ofReal p).toReal⁻¹ ≤ ε ^ p⁻¹
⊢ ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : ↥(lp G 2)
c : 𝕜
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by simp only [inner_smul_left]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
D : RankOneDecomposition 𝕜 X
n : ℕ
x : X
S : X →ₗ[𝕜] X := ↑(succSub D.P n)
hrank : Module.finrank 𝕜 ↥S.range = 1
⊢ ∃ c, c • D.e n = (succSub D.P n) x

Tactic:
have : FiniteDimensional 𝕜 S.range := .of_finrank_pos (hrank.symm ▸ zero_lt_one)

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
D : RankOneDecomposition 𝕜 X
n : ℕ
x : X
S : X →ₗ[𝕜] X := ↑(succSub D.P n)
hrank : Module.finrank 𝕜 ↥S.range = 1
this : FiniteDimensional 𝕜 ↥S.range
⊢ ∃ c, c • D.e n = (succSub D.P n) x
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: 𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)
⊢ ⊤ ≤ K ⊔ bif false then K else Kᗮ

Tactic:
cond

Goal state after:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)
⊢ ⊤ ≤ K ⊔ Kᗮ
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun x ↦ 𝕜) 2)
H : (fun i ↦ ↑f i • b i) = fun b_1 ↦ ↑b.repr.symm ((fun i ↦ lp.single 2 i (↑f i)) b_1)
⊢ HasSum (fun i ↦ ↑f i • b i) (b.repr.symm f)

Tactic:
by
    rw [H]
    have : HasSum (fun i : ι => lp.single 2 i (f i)) f := lp.hasSum_single ENNReal.ofNat_ne_top f
    exact (↑b.repr.symm.toContinuousLinearEquiv : ℓ²(ι, 𝕜) →L[𝕜] E).hasSum this

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun x ↦ 𝕜) 2)
⊢ HasSum (fun i ↦ ↑f i • b i) (b.repr.symm f)

Tactic:
classical
  suffices H : (fun i : ι => f i • b i) = fun b_1 : ι => b.repr.symm.toContinuousLinearEquiv <|
      (fun i : ι => lp.single 2 i (f i) (E := (fun _ : ι => 𝕜))) b_1 by
    rw [H]
    have : HasSum (fun i : ι => lp.single 2 i (f i)) f := lp.hasSum_single ENNReal.ofNat_ne_top f
    exact (↑b.repr.symm.toContinuousLinearEquiv : ℓ²(ι, 𝕜) →L[𝕜] E).hasSum this
  ext i
  apply b.repr.injective
  let : NormedSpace 𝕜 (lp (fun _i : ι => 𝕜) 2) := by infer_instance
  have : lp.single (E := (fun _ : ι => 𝕜)) 2 i (f i * 1) = f i • lp.single 2 i 1 :=
    lp.single_smul (E := (fun _ : ι => 𝕜)) 2 i (f i) (1 : 𝕜)
  rw [mul_one] at this
  rw [map_smul, b.repr_self, ← this, LinearIsometryEquiv.coe_toContinuousLinearEquiv]
  exact (b.repr.apply_symm_apply (lp.single 2 i (f i))).symm

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

Goal state before:
pp: case e_a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ∫ (x : ℝ) in ?a..?a + T, (fourier (-n)) ↑x • liftIoc T a f ↑x = ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x

Tactic:
refine intervalIntegral.integral_congr_ae (ae_of_all _ fun x hx => ?_)

Goal state after:
case e_a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
x : ℝ
hx : x ∈ uIoc a (a + T)
⊢ (fourier (-n)) ↑x • liftIoc T a f ↑x = (fourier (-n)) ↑x • 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
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
hf : Integrable f μ
h'f : Differentiable ℝ f
hf' : Integrable (fderiv ℝ f) μ
w : W
y : V
g : V → ℂ := fun v ↦ ↑(𝐞 (-(L v) w))
this : ∫ (x : V), g x • (fderiv ℝ f x) y ∂μ = ∫ (x : V), (2 * ↑π * I * ↑((L y) w) * g x) • f x ∂μ
⊢ (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fderiv ℝ f) w) y =
    (fourierSMulRight (-L.flip) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w) y

Tactic:
fourierIntegral_continuousLinearMap_apply' hf'

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
hf : Integrable f μ
h'f : Differentiable ℝ f
hf' : Integrable (fderiv ℝ f) μ
w : W
y : V
g : V → ℂ := fun v ↦ ↑(𝐞 (-(L v) w))
this : ∫ (x : V), g x • (fderiv ℝ f x) y ∂μ = ∫ (x : V), (2 * ↑π * I * ↑((L y) w) * g x) • f x ∂μ
⊢ fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun x ↦ (fderiv ℝ f x) y) w =
    (fourierSMulRight (-L.flip) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w) y
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✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
k : ℕ
x₀ : E
this : ‖x₀‖ ^ k * ‖iteratedFDeriv ℝ 0 (⇑f) x₀‖ ≤ (SchwartzMap.seminorm 𝕜 k 0) f
⊢ ‖x₀‖ ^ k * ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 k 0) f

Tactic:
rwa [norm_iteratedFDeriv_zero] at this

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

Goal state before:
pp: case h1
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 : ℕ
m : Fin n → W
i : Fin n
_hi : i ∈ Finset.univ
⊢ |(L v) (m i)| ≤ ‖L‖ * ‖v‖ * ‖m i‖

Tactic:
exact L.le_opNorm₂ v (m i)

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₀
⊢ Tendsto (fun n ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) atTop (𝓝 (g x₀))

Tactic:
have : x₀ ∈ s := by rw [← hs.isClosed.closure_eq]; exact closure_mono interior_subset h₀
  apply
    tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos hs _ hc
      h'c hnc hnc₀ this hmg hcg
  intro u u_open x₀_u
  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.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
⊢ Tendsto (fun c ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)

Tactic:
← h'φ

Goal state after:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
⊢ Tendsto (fun c ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 (∫ (x : F), φ x ∂μ))
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_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.MeasureTheory.Integral.Asymptotics

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup E
f : α → E
g : α → F
a : α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
inst✝² : LinearOrder α
inst✝¹ : CompactIccSpace α
inst✝ : atTop.IsMeasurablyGenerated
hf : LocallyIntegrableOn f (Ici a) μ
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ IntegrableOn f (Ici a) μ

Tactic:
by
  refine integrableOn_Ici_iff_integrableAtFilter_atTop.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩
  exact ⟨Ici a, Ici_mem_atTop a, hf.aestronglyMeasurable⟩

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (deriv f) volume
x : ℝ
I : Integrable (fun x ↦ fderiv ℝ f x) volume
⊢ 𝓕 (deriv f) x = (𝓕 (fderiv ℝ f) x) 1

Tactic:
simp only [fourier_continuousLinearMap_apply I, fderiv_apply_one_eq_deriv]

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

Goal state before:
pp: b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (Ioi 0)
x : ℝ
hx : x ∈ Ioi 0
h'x : 0 ≤ x
⊢ ‖(-x) ^ s * rexp (-b * x ^ 2)‖ ≤ x ^ s * rexp (-b * x ^ 2)

Tactic:
Real.norm_eq_abs,

Goal state after:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (Ioi 0)
x : ℝ
hx : x ∈ Ioi 0
h'x : 0 ≤ x
⊢ |(-x) ^ s * rexp (-b * x ^ 2)| ≤ x ^ s * rexp (-b * x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ × ℝ → E
⊢ ∫ (p : ℝ × ℝ), f p = ∫ (p : ℝ × ℝ) in polarCoord.source, f p

Tactic:
rw [← setIntegral_univ]
      apply setIntegral_congr_set
      exact polarCoord_source_ae_eq_univ.symm

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

Goal state before:
pp: ι : 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

pp: ι : Type u_1
inst✝ : Fintype ι
⊢ Set ι

Tactic:
exact ae_eq_set_pi fun _ _ ↦ polarCoord_source_ae_eq_univ

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

Goal state before:
pp: s : ℂ
h2 : s ≠ 0
⊢ Gamma (s + 1) = s * Gamma s

Tactic:
let n := ⌊1 - s.re⌋₊

Goal state after:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
⊢ Gamma (s + 1) = s * Gamma s
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)
x : ℝ
hx : 0 < x
⊢ ↑x ^ (a - 1) * cexp (-(↑r * ↑x)) = (1 / ↑r) ^ (a - 1) * ↑r ^ (a - 1) * ↑x ^ (a - 1) * cexp (-(↑r * ↑x))

Tactic:
one_div,

Goal state after:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)
x : ℝ
hx : 0 < x
⊢ ↑x ^ (a - 1) * cexp (-(↑r * ↑x)) = (↑r)⁻¹ ^ (a - 1) * ↑r ^ (a - 1) * ↑x ^ (a - 1) * cexp (-(↑r * ↑x))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: case e_a
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
⊢ (1 / b) ^ (1 / 2) = 1 / b ^ (1 / 2)

Tactic:
one_div,

Goal state after:
case e_a
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
⊢ b⁻¹ ^ (1 / 2) = 1 / b ^ (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

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

Tactic:
one_div,

Goal state after:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ι → ℂ
⊢ ∏ x, (↑π / b) ^ 2⁻¹ * cexp (c x ^ 2 / (4 * b)) = (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp ((∑ i, c i ^ 2) / (4 * b))
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:
← fourier_evalCLM_eq

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 : V
⊢ 𝓕 ((SchwartzMap.evalCLM ℝ V E m) (-(2 * ↑π * Complex.I) • (smulRightCLM ℂ E (innerSL ℝ)) f)) =
    𝓕 (-(2 * ↑π * Complex.I) • (smulLeftCLM E fun x ↦ inner ℝ x m) f)