mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Distribution.TestFunction

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
m : MeasurableSpace E
inst✝¹¹ : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst✝¹⁰ : NormedAddCommGroup F₁
inst✝⁹ : NormedSpace 𝕜 F₁
inst✝⁸ : NormedSpace ℝ F₁
inst✝⁷ : NormedAddCommGroup F₂
inst✝⁶ : NormedSpace 𝕜 F₂
inst✝⁵ : NormedAddCommGroup F₃
inst✝⁴ : NormedSpace 𝕜 F₃
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : IsScalarTower ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : LocallyIntegrableOn φ (↑Ω) μ
K : Compacts E
K_sub_Ω : ↑K ⊆ ↑Ω
f : 𝓓^{n}_{K}(E, F₁)
⊢ (integralAgainstBilinCLM B μ φ) (ofSupportedIn K_sub_Ω f) = (ContDiffMapSupportedIn.integralAgainstBilinCLM B μ φ) f

Tactic:
have hφ' := hφ.integrableOn_compact_subset K_sub_Ω K.isCompact
  simp [hφ, hφ']

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

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this : ContDiffAt ℝ (↑n) (fun x ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h✝ : r - ↑n < 0
h : 0 < ↑n - r
⊢ Real.exp (Real.log (3 / 2) * ↑k) ≤ (3 / 2) ^ k

Tactic:
by
      rw [← Real.rpow_natCast, Real.rpow_def_of_pos]
      norm_num

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Compact.Basic

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : IsUniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U
⊢ ∀ U ∈ 𝓝 0, ∃ t, t.Finite ∧ ⇑u '' closedBall 0 1 ⊆ ⋃ y ∈ t, y +ᵥ U

Tactic:
intro U hU

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : IsUniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
⊢ ∃ t, t.Finite ∧ ⇑u '' closedBall 0 1 ⊆ ⋃ y ∈ t, y +ᵥ U
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : Nontrivial E
hT : T.IsSymmetric
this✝ : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact (sphere 0 ‖x‖)
H₂ : (sphere 0 ‖x‖).Nonempty
x₀ : E
hx₀' : x₀ ∈ sphere 0 ‖x‖
hTx₀ : IsMaxOn (↑T').reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
this : IsMaxOn (↑T').reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ ‖x₀‖ ≠ 0

Tactic:
simp only [hx₀, norm_eq_zero, hx, Ne, not_false_iff]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : Nontrivial E
hT : T.IsSymmetric
this✝ : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact (sphere 0 ‖x‖)
H₂ : (sphere 0 ‖x‖).Nonempty
x₀ : E
hx₀' : x₀ ∈ sphere 0 ‖x‖
hTx₀ : IsMinOn (↑T').reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
this : IsMinOn (↑T').reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ ‖x₀‖ ≠ 0

Tactic:
simp only [hx₀, norm_eq_zero, hx, Ne, not_false_iff]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h : ∀ c > 0, ∃ x, ‖(T - μ • 1) x‖ < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc : ∀ ε > 0, ∃ x, ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ ‖(T - μ • 1) x‖ < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : ℕ → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), ‖(T - μ • 1) (x n)‖ < φ n
hx_lim : Tendsto (fun n ↦ (T - μ • 1) (x n)) atTop (𝓝 0)
y_ : ℕ → X := fun n ↦ T (x n)
K : Set X
hK : IsCompact K
hK' : ⇑↑T '' Metric.closedBall 0 1 ⊆ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hy_lim : Tendsto (fun n ↦ (T - μ • 1) (y_ n)) atTop (𝓝 0)
d : ℝ
hd₀ : d > 0
hd : ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
hyK : 0 ∈ K
hψy : Tendsto (y_ ∘ ψ) atTop (𝓝 0)
hy_eigen' : (T - μ • 1) 0 = 0
⊢ False

Tactic:
suffices ∀ᶠ n : ℕ in atTop, False by rwa [eventually_const] at this

Goal state after:
𝕜 : Type u_1
X : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h : ∀ c > 0, ∃ x, ‖(T - μ • 1) x‖ < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc : ∀ ε > 0, ∃ x, ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ ‖(T - μ • 1) x‖ < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : ℕ → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), ‖(T - μ • 1) (x n)‖ < φ n
hx_lim : Tendsto (fun n ↦ (T - μ • 1) (x n)) atTop (𝓝 0)
y_ : ℕ → X := fun n ↦ T (x n)
K : Set X
hK : IsCompact K
hK' : ⇑↑T '' Metric.closedBall 0 1 ⊆ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hy_lim : Tendsto (fun n ↦ (T - μ • 1) (y_ n)) atTop (𝓝 0)
d : ℝ
hd₀ : d > 0
hd : ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
hyK : 0 ∈ K
hψy : Tendsto (y_ ∘ ψ) atTop (𝓝 0)
hy_eigen' : (T - μ • 1) 0 = 0
⊢ ∀ᶠ (n : ℕ) in atTop, False
Module: Mathlib.Data.Fin.Tuple.Sort

Goal state before:
pp: n : ℕ
σ : Equiv.Perm (Fin n)
i✝ j✝ : Fin n
⊢ i✝ < j✝ → σ (σ⁻¹ i✝) = σ (σ⁻¹ j✝) → σ⁻¹ i✝ < σ⁻¹ j✝

Tactic:
hij

Goal state after:
n : ℕ
σ : Equiv.Perm (Fin n)
i✝ j✝ : Fin n
hij : i✝ < j✝
⊢ σ (σ⁻¹ i✝) = σ (σ⁻¹ j✝) → σ⁻¹ i✝ < σ⁻¹ j✝
Module: Mathlib.Analysis.Matrix.Hermitian

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype n
inst✝² : DecidableEq n
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : OrthonormalBasis n 𝕜 E
this : FiniteDimensional 𝕜 E
⊢ ((toLin b.toBasis b.toBasis) A).IsSymmetric ↔ A.IsHermitian

Tactic:
simp_rw [LinearMap.IsSymmetric, ← LinearMap.adjoint_inner_left, ← toLin_conjTranspose]

Goal state after:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype n
inst✝² : DecidableEq n
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : OrthonormalBasis n 𝕜 E
this : FiniteDimensional 𝕜 E
⊢ (∀ (x y : E), inner 𝕜 (((toLin b.toBasis b.toBasis) A) x) y = inner 𝕜 (((toLin b.toBasis b.toBasis) Aᴴ) x) y) ↔
    A.IsHermitian
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
inst✝ : LinearMap.CompatibleSMul F F' ℝ 𝕜
T : F →L[𝕜] F'
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
⊢ { toFun := ⇑T ∘ ⇑(c • f), contDiff' := ⋯, zero_on_compl' := ⋯ } =
    (RingHom.id 𝕜) c • { toFun := ⇑T ∘ ⇑f, contDiff' := ⋯, zero_on_compl' := ⋯ }

Tactic:
ext x; exact map_smul T c (f x)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
i : ℕ
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
⊢ (if hi : k + ↑i ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0) =
    (RingHom.id 𝕜) c • if hi : k + ↑i ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0

Tactic:
by
    split_ifs with hi
    · have hi' : (i : ℕ∞ω) ≤ n := mod_cast (le_of_add_le_right hi)
      ext
      simp [iteratedFDeriv_const_smul_apply (f.contDiff.of_le hi').contDiffAt, FunLike.coe_smul]
    · simp

Goal state after:
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
h₁ : A.PosSemidef
h₂ : (-A).PosSemidef
i✝ j i : n
⊢ 0 ≤ A i i

Tactic:
by simpa using h₁.diag_nonneg

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
K : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓_{K}(E, F)
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F ⊤ K i) f ≤ C ↔ ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C

Tactic:
simp_rw [ContDiffMapSupportedIn.seminorm_le_iff 𝕜 hC, le_top, forall_const]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ‖⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * ‖f‖₊

Tactic:
apply Lp.nnnorm_le_of_ae_bound
  refine (f.toContinuousMap.coeFn_toAEEqFun μ).mono ?_
  intro x hx
  rw [← NNReal.coe_le_coe, coe_nnnorm, coe_nnnorm]
  convert! f.norm_coe_le_norm x using 2

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 g : ↥(Lp E 2 μ)
r : 𝕜
⊢ ⟪r • f, g⟫ = (starRingEnd 𝕜) r * ⟪f, g⟫

Tactic:
rw [inner_def, inner_def, ← smul_eq_mul, ← integral_smul]

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 g : ↥(Lp E 2 μ)
r : 𝕜
⊢ ∫ (a : α), ⟪↑↑(r • f) a, ↑↑g a⟫ ∂μ = ∫ (a : α), (starRingEnd 𝕜) r • ⟪↑↑f a, ↑↑g a⟫ ∂μ
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
b : SchauderBasis 𝕜 X
n : ℕ
⊢ (↑(b.proj n)).range = Submodule.span 𝕜 (↑b '' ↑(Finset.range n))

Tactic:
by
  rw [proj, GeneralSchauderBasis.range_proj_eq_span]

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
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : IsHilbertSum 𝕜 G V
w : ↥(lp G 2)
⊢ HasSum (fun i ↦ (V i) (↑w i)) (hV.linearIsometryEquiv.symm w)

Tactic:
simp [IsHilbertSum.linearIsometryEquiv, OrthogonalFamily.hasSum_linearIsometry]

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)
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:
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
x y : E
⊢ HasSum (fun i ↦ ⟪x, b i⟫ * ⟪b i, y⟫) ⟪x, y⟫

Tactic:
convert! (b.hasSum_repr y).mapL (innerSL 𝕜 x) using 1
  ext i
  rw [innerSL_apply_apply, b.repr_apply_apply, inner_smul_right, mul_comm]

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

Goal state before:
pp: case e'_9
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ (fourier (-n)) ↑x = -2 * ↑π * I * ↑n / ↑T * (fourier (-n)) ↑x / (-2 * ↑π * I * ↑n / ↑T)

Tactic:
· simp [mul_div_cancel_left₀, hn, (Fact.out : 0 < T).ne', Real.pi_pos.ne']

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
A : Tendsto (fun δ ↦ δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ) (𝓝[>] 0) (𝓝 (0 * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * 0))
⊢ ∃ δ, δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε ∧ 0 < δ ∧ δ < 1

Tactic:
rw [zero_mul, zero_add, mul_zero] at A

Goal state after:
α : 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
A : Tendsto (fun δ ↦ δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ) (𝓝[>] 0) (𝓝 0)
⊢ ∃ δ, δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε ∧ 0 < δ ∧ δ < 1
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
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
⊢ (‖x‖ + 1) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ 2 ^ m.1 * ((Finset.Iic m).sup fun m ↦ SchwartzMap.seminorm 𝕜 m.1 m.2) f

Tactic:
add_pow

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✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
⊢ (∑ m ∈ Finset.range (k + 1), ‖x‖ ^ m * 1 ^ (k - m) * ↑(k.choose m)) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
    2 ^ m.1 * ((Finset.Iic m).sup fun m ↦ SchwartzMap.seminorm 𝕜 m.1 m.2) f
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 : ℕ
m : Fin n → W
⊢ ‖(fourierPowSMulRight L f v n) m‖ = (2 * π) ^ n * ((∏ x, |(L v) (m x)|) * ‖f v‖)

Tactic:
by
      simp [abs_of_nonneg pi_nonneg, norm_smul]

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' : ℕ := ⋯
f : 𝓢(E, F)
x : D
seminorm_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 + ‖x‖) ^ l ≤ ((1 + ‖x‖) ^ l) ^ N

Tactic:
refine le_self_pow₀ (one_le_pow₀ ?_) hN₁'
      simp only [le_add_iff_nonneg_right, norm_nonneg]

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✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup D
inst✝¹ : NormedSpace ℝ D
inst✝ : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
⊢ ‖x‖ ≤ ↑K * ‖g x - g 0‖

Tactic:
by
    rw [← dist_zero_right, ← dist_eq_norm]
    apply h'g.le_mul_dist

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 φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
⊢ δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) < δ ^ finrank ℝ F * ε

Tactic:
calc
      δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x))
      _ ≤ ‖x‖ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) := by
        gcongr; exact mul_nonneg (by positivity) (hφ _)
      _ = ‖c • x‖ ^ finrank ℝ F * φ (c • x) := by
        simp [norm_smul, abs_of_pos cpos, mul_pow]; ring
      _ < δ ^ finrank ℝ F * ε := by
        apply hM
        rw [div_lt_iff₀ δpos] at hc
        simp only [mem_compl_iff, mem_closedBall, dist_zero_right, norm_smul, Real.norm_eq_abs,
          abs_of_nonneg cpos.le, not_le]
        exact hc.trans_le (by gcongr)

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
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 ν
hG : CompleteSpace G
⊢ ∫ (ξ : W), (M.flip (g ξ)) (∫ (x : V), e (-(L x) ξ) • f x ∂μ) ∂ν =
    ∫ (ξ : W), ∫ (x : V), (M.flip (g ξ)) (e (-(L x) ξ) • f x) ∂μ ∂ν

Tactic:
congr with ξ
    apply (ContinuousLinearMap.integral_comp_comm _ _).symm
    exact (fourierIntegral_convergent_iff he hL _).2 hf

Goal state after:
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
⊢ (fun a ↦ 𝐞 (-⟪a, x⟫) • ↑↑(c • f) a) =ᵐ[volume] fun a ↦ (RingHom.id ℂ) c • 𝐞 (-⟪a, x⟫) • ↑↑f a

Tactic:
filter_upwards [Lp.coeFn_smul c f] with x h

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✝ x : V
h : ↑↑(c • f) x = (c • ↑↑f) x
⊢ 𝐞 (-⟪x, x✝⟫) • ↑↑(c • f) x = (RingHom.id ℂ) c • 𝐞 (-⟪x, x✝⟫) • ↑↑f x
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn (fun x ↦ x ^ s * rexp (-b * x ^ 2)) (Iio 0) volume

Tactic:
rw [← (Measure.measurePreserving_neg (volume : Measure ℝ)).integrableOn_comp_preimage
      (Homeomorph.neg ℝ).measurableEmbedding]

Goal state after:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn ((fun x ↦ x ^ s * rexp (-b * x ^ 2)) ∘ Neg.neg) (Neg.neg ⁻¹' Iio 0) volume
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
F_der_I :
  ∀ x ∈ Ioo 0 X,
    HasDerivAt (fun x ↦ ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x
cont : Continuous ((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s)
der_ible : IntervalIntegrable (fun x ↦ -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X
int_eval :
  ∫ (y : ℝ) in 0..X, -(↑(rexp (-y)) * ↑y ^ s) + ↑(rexp (-y)) * (s * ↑y ^ (s - 1)) =
    ((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s) X - ((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s) 0
⊢ ∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * ↑x ^ s =
    (s * ∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * ↑x ^ (s - 1)) - ↑(rexp (-X)) * ↑X ^ s

Tactic:
apply_fun fun x : ℂ => -x at int_eval

Goal state after:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
F_der_I :
  ∀ x ∈ Ioo 0 X,
    HasDerivAt (fun x ↦ ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x
cont : Continuous ((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s)
der_ible : IntervalIntegrable (fun x ↦ -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X
int_eval :
  -∫ (y : ℝ) in 0..X, -(↑(rexp (-y)) * ↑y ^ s) + ↑(rexp (-y)) * (s * ↑y ^ (s - 1)) =
    -(((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s) X - ((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s) 0)
⊢ ∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * ↑x ^ s =
    (s * ∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * ↑x ^ (s - 1)) - ↑(rexp (-X)) * ↑X ^ s