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

Goal state before:
pp: case h.hg₁
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
this✝ : MemLp (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)) 2 volume
this : MemLp (fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-s / 2))) 2 volume
⊢ Function.HasTemperateGrowth fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-s / 2))

Tactic:
·

Goal state after:
case h.hg₁
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
this✝ : MemLp (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)) 2 volume
this : MemLp (fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-s / 2))) 2 volume
⊢ Function.HasTemperateGrowth fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-s / 2))
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Fintype α
ι : Type
w✝ : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
i : ι
⊢ NeZero (n i)

Tactic:
have := hn i

Goal state after:
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Fintype α
ι : Type
w✝ : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
i : ι
this : 1 < n i
⊢ NeZero (n i)
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
⊢ (∃ ψ, ψ a ≠ 1) → a ≠ 0

pp: case refine_2
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
ha : a ≠ 0
⊢ ∃ ψ, ψ a ≠ 1

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
⊢ (∃ ψ, ψ a ≠ 1) → a ≠ 0
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: p : ℕ+
⊢ p.Prime → p ≠ 1

Tactic:
intro pp

Goal state after:
p : ℕ+
pp : p.Prime
⊢ p ≠ 1
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case e'_2
f : C(ℝ, ℂ)
h_norm : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n ↦ 𝓕 ⇑f ↑n
x : ℝ
F : C(UnitAddCircle, ℂ) := { toFun := ⋯.lift, continuous_toFun := ⋯ }
this : Summable (fourierCoeff ⇑F)
⊢ ∑' (n : ℤ), f (x + ↑n) = F ↑x

pp: case e'_3
f : C(ℝ, ℂ)
h_norm : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n ↦ 𝓕 ⇑f ↑n
x : ℝ
F : C(UnitAddCircle, ℂ) := { toFun := ⋯.lift, continuous_toFun := ⋯ }
this : Summable (fourierCoeff ⇑F)
⊢ ∑' (n : ℤ), 𝓕 ⇑f ↑n * (fourier n) ↑x = ∑' (b : ℤ), fourierCoeff (⇑F) b • (fourier b) ↑x

Tactic:
·

Goal state after:
case e'_2
f : C(ℝ, ℂ)
h_norm : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n ↦ 𝓕 ⇑f ↑n
x : ℝ
F : C(UnitAddCircle, ℂ) := { toFun := ⋯.lift, continuous_toFun := ⋯ }
this : Summable (fourierCoeff ⇑F)
⊢ ∑' (n : ℤ), f (x + ↑n) = F ↑x
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case e'_3
f : C(ℝ, ℂ)
h_norm : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n ↦ 𝓕 ⇑f ↑n
x : ℝ
F : C(UnitAddCircle, ℂ) := { toFun := ⋯.lift, continuous_toFun := ⋯ }
this : Summable (fourierCoeff ⇑F)
⊢ ∑' (n : ℤ), 𝓕 ⇑f ↑n * (fourier n) ↑x = ∑' (b : ℤ), fourierCoeff (⇑F) b • (fourier b) ↑x

Tactic:
·

Goal state after:
case e'_3
f : C(ℝ, ℂ)
h_norm : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n ↦ 𝓕 ⇑f ↑n
x : ℝ
F : C(UnitAddCircle, ℂ) := { toFun := ⋯.lift, continuous_toFun := ⋯ }
this : Summable (fourierCoeff ⇑F)
⊢ ∑' (n : ℤ), 𝓕 ⇑f ↑n * (fourier n) ↑x = ∑' (b : ℤ), fourierCoeff (⇑F) b • (fourier b) ↑x
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: n : ℕ+
⊢ gcd 1 n = 1

Tactic:
by
  rw [gcd_eq_left_iff_dvd]
  apply one_dvd

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

Goal state before:
pp: case mp
n : ℕ
h : μ n ≠ 0
⊢ Squarefree n

pp: case mpr
n : ℕ
h : Squarefree n
⊢ μ n ≠ 0

Tactic:
·

Goal state after:
case mp
n : ℕ
h : μ n ≠ 0
⊢ Squarefree n
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case mpr
n : ℕ
h : Squarefree n
⊢ μ n ≠ 0

Tactic:
·

Goal state after:
case mpr
n : ℕ
h : Squarefree n
⊢ μ n ≠ 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case pos
n : ℕ
h✝ : Squarefree n
⊢ (-1) ^ cardFactors n = 0 ∨ (-1) ^ cardFactors n = 1 ∨ (-1) ^ cardFactors n = -1

pp: case neg
n : ℕ
h✝ : ¬Squarefree n
⊢ 0 = 0 ∨ 0 = 1 ∨ False

Tactic:
·

Goal state after:
case pos
n : ℕ
h✝ : Squarefree n
⊢ (-1) ^ cardFactors n = 0 ∨ (-1) ^ cardFactors n = 1 ∨ (-1) ^ cardFactors n = -1
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case neg
n : ℕ
h✝ : ¬Squarefree n
⊢ 0 = 0 ∨ 0 = 1 ∨ False

Tactic:
·

Goal state after:
case neg
n : ℕ
h✝ : ¬Squarefree n
⊢ 0 = 0 ∨ 0 = 1 ∨ False
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case pos
n : ℕ
h : Squarefree n
⊢ μ n ^ 2 = 1

pp: case neg
n : ℕ
h : ¬Squarefree n
⊢ μ n ^ 2 = 0

Tactic:
·

Goal state after:
case pos
n : ℕ
h : Squarefree n
⊢ μ n ^ 2 = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case neg
n : ℕ
h : ¬Squarefree n
⊢ μ n ^ 2 = 0

Tactic:
·

Goal state after:
case neg
n : ℕ
h : ¬Squarefree n
⊢ μ n ^ 2 = 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case pos
n : ℕ
h : Squarefree n
⊢ |μ n| = 1

pp: case neg
n : ℕ
h : ¬Squarefree n
⊢ |μ n| = 0

Tactic:
·

Goal state after:
case pos
n : ℕ
h : Squarefree n
⊢ |μ n| = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case neg
n : ℕ
h : ¬Squarefree n
⊢ |μ n| = 0

Tactic:
·

Goal state after:
case neg
n : ℕ
h : ¬Squarefree n
⊢ |μ n| = 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case pos
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : k = 1
⊢ μ (p ^ k) = -1

pp: case neg
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ μ (p ^ k) = 0

Tactic:
·

Goal state after:
case pos
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : k = 1
⊢ μ (p ^ k) = -1
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
w : V
hw : w ≠ 0
hf : Integrable f volume
⊢ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v = (1 / 2 * 2) • ∫ (a : V), 𝐞 (-⟪a, w⟫) • f a

pp: case hf
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
w : V
hw : w ≠ 0
hf : Integrable f volume
⊢ Integrable (fun v ↦ 𝐞 (-⟪v, w⟫) • f v) volume

pp: case hg
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
w : V
hw : w ≠ 0
hf : Integrable f volume
⊢ Integrable (fun v ↦ 𝐞 (-⟪v, w⟫) • f (v + (1 / (2 * ‖w‖ ^ 2)) • w)) volume

Tactic:
·

Goal state after:
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
w : V
hw : w ≠ 0
hf : Integrable f volume
⊢ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v = (1 / 2 * 2) • ∫ (a : V), 𝐞 (-⟪a, w⟫) • f a
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
⊢ ∏ p ∈ n.primeFactors, (1 + f p) = (ArithmeticFunction.prodPrimeFactors fun p ↦ (↑ζ + f) p) n

pp: R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ (ArithmeticFunction.prodPrimeFactors fun p ↦ (↑ζ + f) p) n = ∑ d ∈ n.divisors, f d

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 + f p) = (ArithmeticFunction.prodPrimeFactors fun p ↦ (↑ζ + f) p) n
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
⊢ ∏ p ∈ n.primeFactors, (1 - f p) = ∏ p ∈ n.primeFactors, (1 + ((↑μ).pmul f) p)

pp: R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 + ((↑μ).pmul f) p) = ∑ d ∈ n.divisors, ↑(μ d) * f d

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 - f p) = ∏ p ∈ n.primeFactors, (1 + ((↑μ).pmul f) p)
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
⊢ ∏ p ∈ n.primeFactors, (1 + ((↑μ).pmul f) p) = ∑ d ∈ n.divisors, ↑(μ d) * f d

Tactic:
·

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

Goal state before:
pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ↑ζ • f' = g'

pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ ↑ζ • f' = g' ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ↑ζ • f' = g'
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ ↑ζ • f' = g' ↔ μ • g' = f'

pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ μ • g' = f' ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ ↑ζ • f' = g' ↔ μ • g' = f'
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ μ • g' = f' ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ μ • g' = f' ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
⊢ ∏ i ∈ n.divisors, f i = g n ↔
    (∏ i ∈ n.divisors, if h : 0 < i then Units.mk0 (f i) ⋯ else 1) = if h : 0 < n then Units.mk0 (g n) ⋯ else 1

pp: case refine_2
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
⊢ (∏ x ∈ n.divisorsAntidiagonal, (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1 =
      if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
    ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
⊢ ∏ i ∈ n.divisors, f i = g n ↔
    (∏ i ∈ n.divisors, if h : 0 < i then Units.mk0 (f i) ⋯ else 1) = if h : 0 < n then Units.mk0 (g n) ⋯ else 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
⊢ (∏ x ∈ n.divisorsAntidiagonal, (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1 =
      if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
    ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
⊢ (∏ x ∈ n.divisorsAntidiagonal, (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1 =
      if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
    ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n
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
⊢ (∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n) → ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

pp: case mpr
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ (∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n) → ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n

Tactic:
·

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
⊢ (∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n) → ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case e'_3
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ (b_1 : ℝ), d ≤ b_1 → ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ |↑y| = ↑y

pp: case e'_4
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ (b_1 : ℝ), d ≤ b_1 → ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ |x| = x

Tactic:
·

Goal state after:
case e'_3
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ (b_1 : ℝ), d ≤ b_1 → ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ |↑y| = ↑y
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case e'_4
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ (b_1 : ℝ), d ≤ b_1 → ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ |x| = x

Tactic:
·

Goal state after:
case e'_4
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ (b_1 : ℝ), d ≤ b_1 → ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ |x| = x
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

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

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ (∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n) → ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case mpr
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 → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
F : ℕ → R := fun n ↦ ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2
n : ℕ
hn : n > 0
hnP : n ∈ s
⊢ ∑ i ∈ n.divisors, f i = g n

Tactic:
suffices ∑ d ∈ n.divisors, F d = g n by
      rw [← 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 mpr
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 → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
F : ℕ → R := fun n ↦ ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2
n : ℕ
hn : n > 0
hnP : n ∈ s
⊢ ∑ d ∈ n.divisors, F d = g n
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x ↦ |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ }) =O[atTop] fun x ↦ |x| ^ (-b)
h2 :
  ((fun x ↦ ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x ↦ |x| ^ (-b)
this : (fun x ↦ |x| ^ (-b)) ∘ Neg.neg = fun x ↦ |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ ‖f x‖ =
    ‖(ContinuousMap.restrict (Icc (-x✝ + -S) (-x✝ + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ }))
        ⟨-x, ?refine_2⟩‖

pp: case refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x ↦ |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ }) =O[atTop] fun x ↦ |x| ^ (-b)
h2 :
  ((fun x ↦ ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x ↦ |x| ^ (-b)
this : (fun x ↦ |x| ^ (-b)) ∘ Neg.neg = fun x ↦ |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ∈ Icc (-x✝ + -S) (-x✝ + -R)

Tactic:
·

Goal state after:
case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x ↦ |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ }) =O[atTop] fun x ↦ |x| ^ (-b)
h2 :
  ((fun x ↦ ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x ↦ |x| ^ (-b)
this : (fun x ↦ |x| ^ (-b)) ∘ Neg.neg = fun x ↦ |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ ‖f x‖ =
    ‖(ContinuousMap.restrict (Icc (-x✝ + -S) (-x✝ + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ }))
        ⟨-x, ?refine_2⟩‖
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
⊢ n ∈ s → ∏ i ∈ n.divisors, f i = g n ↔
    n ∈ s → (∏ i ∈ n.divisors, if h : 0 < i then Units.mk0 (f i) ⋯ else 1) = if h : 0 < n then Units.mk0 (g n) ⋯ else 1

pp: case refine_2
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
⊢ (n ∈ s →
      ∏ x ∈ n.divisorsAntidiagonal, (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1 =
        if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
    n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
⊢ n ∈ s → ∏ i ∈ n.divisors, f i = g n ↔
    n ∈ s → (∏ i ∈ n.divisors, if h : 0 < i then Units.mk0 (f i) ⋯ else 1) = if h : 0 < n then Units.mk0 (g n) ⋯ else 1
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x ↦ |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ }) =O[atTop] fun x ↦ |x| ^ (-b)
h2 :
  ((fun x ↦ ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x ↦ |x| ^ (-b)
this : (fun x ↦ |x| ^ (-b)) ∘ Neg.neg = fun x ↦ |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ∈ Icc (-x✝ + -S) (-x✝ + -R)

Tactic:
·

Goal state after:
case refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x ↦ |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ }) =O[atTop] fun x ↦ |x| ^ (-b)
h2 :
  ((fun x ↦ ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x ↦ |x| ^ (-b)
this : (fun x ↦ |x| ^ (-b)) ∘ Neg.neg = fun x ↦ |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ∈ Icc (-x✝ + -S) (-x✝ + -R)
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
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
⊢ ‖∫ (v : V), 𝐞 (-⟪v, w⟫) • f v‖ < ε

Tactic:
rw [fourierIntegral_eq_half_sub_half_period_translate hw_ne
      (hf1.integrable_of_hasCompactSupport hf2),
    norm_smul, this, inv_mul_eq_div, div_lt_iff₀' two_pos]

Goal state after:
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
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
⊢ ‖∫ (v : V), 𝐞 (-⟪v, w⟫) • (f v - f (v + i w))‖ < 2 * ε