awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
p : (f : ↥(Lp F 2 volume)) → Prop :=
  fun (f : ↥(Lp F 2 volume)) ↦ 𝓕 (E := 𝓢'(E, F)) (toTemperedDistribution f) = toTemperedDistribution (𝓕 f)
hp : IsClosed (X := ↥(Lp F 2 volume)) {b : ↥(Lp F 2 volume) | p b}
ih : ∀ (a : 𝓢(E, F)), p ((toLpCLM ℝ F 2 volume : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) a)
⊢ 𝓕 (E := 𝓢'(E, F)) (toTemperedDistribution f) = toTemperedDistribution (𝓕 f)

Tactic:
apply DenseRange.induction_on (p := p)
    (SchwartzMap.denseRange_toLpCLM (p := 2) ENNReal.ofNat_ne_top) f

Premises used: ENNReal.ofNat_ne_top, SchwartzMap.denseRange_toLpCLM, DenseRange.induction_on
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
p : (f : ↥(Lp F 2 volume)) → Prop :=
  fun (f : ↥(Lp F 2 volume)) ↦ 𝓕 (E := 𝓢'(E, F)) (toTemperedDistribution f) = toTemperedDistribution (𝓕 f)
hp : Continuous (Y := 𝓢'(E, F)) fun (y : ↥(Lp F 2 volume)) ↦ 𝓕 (E := 𝓢'(E, F)) (toTemperedDistribution y)
hp₁ : Continuous (Y := 𝓢'(E, F)) fun (y : ↥(Lp F 2 volume)) ↦ toTemperedDistribution (𝓕 y)
⊢ IsClosed (X := ↥(Lp F 2 volume)) {b : ↥(Lp F 2 volume) | p b}

Tactic:
apply isClosed_eq

Premises used: isClosed_eq
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
p : (f : ↥(Lp F 2 volume)) → Prop :=
  fun (f : ↥(Lp F 2 volume)) ↦ 𝓕 (E := 𝓢'(E, F)) (toTemperedDistribution f) = toTemperedDistribution (𝓕 f)
⊢ Continuous (Y := 𝓢'(E, F)) fun (y : ↥(Lp F 2 volume)) ↦ 𝓕 (E := 𝓢'(E, F)) (toTemperedDistribution y)

Tactic:
(fourierCLM ℂ 𝓢'(E, F) ∘L toTemperedDistributionCLM F volume 2).continuous

Premises used: ContinuousLinearMap.comp, MeasureTheory.Lp.toTemperedDistributionCLM, FourierTransform.fourierCLM, ContinuousLinearMap.continuous, MeasureTheory.MeasureSpace.volume, TemperedDistribution, Complex, OfNat.ofNat
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
p : (f : ↥(Lp F 2 volume)) → Prop :=
  fun (f : ↥(Lp F 2 volume)) ↦ 𝓕 (E := 𝓢'(E, F)) (toTemperedDistribution f) = toTemperedDistribution (𝓕 f)
⊢ Continuous (Y := 𝓢'(E, F)) fun (y : ↥(Lp F 2 volume)) ↦ 𝓕 (E := 𝓢'(E, F)) (toTemperedDistribution y)

Tactic:
exact (fourierCLM ℂ 𝓢'(E, F) ∘L toTemperedDistributionCLM F volume 2).continuous

Premises used: ContinuousLinearMap.comp, MeasureTheory.Lp.toTemperedDistributionCLM, FourierTransform.fourierCLM, ContinuousLinearMap.continuous, MeasureTheory.MeasureSpace.volume, TemperedDistribution, Complex, OfNat.ofNat
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
p : (f : ↥(Lp F 2 volume)) → Prop :=
  fun (f : ↥(Lp F 2 volume)) ↦ 𝓕 (E := 𝓢'(E, F)) (toTemperedDistribution f) = toTemperedDistribution (𝓕 f)
⊢ Continuous (Y := 𝓢'(E, F)) fun (y : ↥(Lp F 2 volume)) ↦ toTemperedDistribution (𝓕 y)

Tactic:
(toTemperedDistributionCLM F volume 2 ∘L fourierCLM ℂ (Lp (α := E) F 2)).continuous

Premises used: ContinuousLinearMap.comp, Set.Mem, setOf, Membership.mem, MeasureTheory.Lp.toTemperedDistributionCLM, Subtype, MeasureTheory.Lp, FourierTransform.fourierCLM, ContinuousLinearMap.continuous, MeasureTheory.MeasureSpace.volume, MeasureTheory.Lp.toTemperedDistribution, Complex, OfNat.ofNat
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
p : (f : ↥(Lp F 2 volume)) → Prop :=
  fun (f : ↥(Lp F 2 volume)) ↦ 𝓕 (E := 𝓢'(E, F)) (toTemperedDistribution f) = toTemperedDistribution (𝓕 f)
⊢ Continuous (Y := 𝓢'(E, F)) fun (y : ↥(Lp F 2 volume)) ↦ toTemperedDistribution (𝓕 y)

Tactic:
exact (toTemperedDistributionCLM F volume 2 ∘L fourierCLM ℂ (Lp (α := E) F 2)).continuous

Premises used: ContinuousLinearMap.comp, Membership.mem, MeasureTheory.Lp.toTemperedDistributionCLM, Subtype, MeasureTheory.Lp, FourierTransform.fourierCLM, ContinuousLinearMap.continuous, MeasureTheory.MeasureSpace.volume, Complex, OfNat.ofNat
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f_1 : ↥(Lp F 2 volume)
p : (f : ↥(Lp F 2 volume)) → Prop :=
  fun (f : ↥(Lp F 2 volume)) ↦ 𝓕 (E := 𝓢'(E, F)) (toTemperedDistribution f) = toTemperedDistribution (𝓕 f)
f : 𝓢(E, F)
⊢ p ((toLpCLM ℝ F 2 volume : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) f)

Tactic:
simp [p, TemperedDistribution.fourier_toTemperedDistributionCLM_eq]

Premises used: TemperedDistribution.fourier_toTemperedDistributionCLM_eq
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
e_a : f = 𝓕 (𝓕⁻ f)
⊢ 𝓕⁻ (E := 𝓢'(E, F)) (toTemperedDistribution f) = 𝓕⁻ (E := 𝓢'(E, F)) (toTemperedDistribution (𝓕 (𝓕⁻ f)))

Tactic:
congr
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
⊢ f = 𝓕 (𝓕⁻ f)

Tactic:
(fourier_fourierInv_eq f).symm

Premises used: FourierInvPair.fourier_fourierInv_eq, Eq.symm
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
⊢ f = 𝓕 (𝓕⁻ f)

Tactic:
exact (fourier_fourierInv_eq f).symm

Premises used: FourierInvPair.fourier_fourierInv_eq, Eq.symm
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
rw rw₁ : 𝓕⁻ (E := 𝓢'(E, F)) (toTemperedDistribution (𝓕 (𝓕⁻ f))) = 𝓕⁻ (E := 𝓢'(E, F)) (toTemperedDistribution (𝓕 (𝓕⁻ f)))
⊢ 𝓕⁻ (E := 𝓢'(E, F)) (toTemperedDistribution (𝓕 (𝓕⁻ f))) = 𝓕⁻ (𝓕 (E := 𝓢'(E, F)) (toTemperedDistribution (𝓕⁻ f)))

Tactic:
rw [fourier_toTemperedDistribution_eq]

Premises used: MeasureTheory.Lp.fourier_toTemperedDistribution_eq
-- Module: Mathlib.Analysis.Fourier.Notation
Goal:
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : AddCommGroup F
inst_2 : FourierTransform E F
inst_3 : FourierAdd E F
⊢ fourier.{u_3, u_4} (E := E) 0 = 0

Tactic:
map_zero (AddMonoidHom.mk' 𝓕 fourier_add)

Premises used: map_zero, FourierTransform.fourier, FourierAdd.fourier_add, AddMonoidHom.mk'
-- Module: Mathlib.Analysis.Fourier.Notation
Goal:
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : AddCommGroup F
inst_2 : FourierTransform E F
inst_3 : FourierAdd E F
f : E
⊢ 𝓕 (-f) = -𝓕 f

Tactic:
map_neg (AddMonoidHom.mk' 𝓕 fourier_add) f

Premises used: map_neg, FourierTransform.fourier, FourierAdd.fourier_add, AddMonoidHom.mk'
-- Module: Mathlib.Analysis.Fourier.Notation
Goal:
ι : Type u_1
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : AddCommGroup F
inst_2 : FourierTransform E F
inst_3 : FourierAdd E F
f : ι → E
s : Finset ι
⊢ fourier.{u_3, u_4} (E := E) (∑ i ∈ s, f i) = ∑ i ∈ s, 𝓕 (f i)

Tactic:
map_sum (AddMonoidHom.mk' 𝓕 fourier_add) f s

Premises used: map_sum, FourierTransform.fourier, FourierAdd.fourier_add, AddMonoidHom.mk'
-- Module: Mathlib.Analysis.Fourier.Notation
Goal:
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : AddCommGroup F
inst_2 : FourierTransformInv E F
inst_3 : FourierInvAdd E F
⊢ fourierInv.{u_3, u_4} (E := E) 0 = 0

Tactic:
map_zero (AddMonoidHom.mk' 𝓕⁻ fourierInv_add)

Premises used: map_zero, FourierInvAdd.fourierInv_add, FourierTransformInv.fourierInv, AddMonoidHom.mk'
-- Module: Mathlib.Analysis.Fourier.Notation
Goal:
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : AddCommGroup F
inst_2 : FourierTransformInv E F
inst_3 : FourierInvAdd E F
f : E
⊢ 𝓕⁻ (-f) = -𝓕⁻ f

Tactic:
map_neg (AddMonoidHom.mk' 𝓕⁻ fourierInv_add) f

Premises used: FourierInvAdd.fourierInv_add, map_neg, FourierTransformInv.fourierInv, AddMonoidHom.mk'
-- Module: Mathlib.Analysis.Fourier.Notation
Goal:
ι : Type u_1
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : AddCommGroup F
inst_2 : FourierTransformInv E F
inst_3 : FourierInvAdd E F
f : ι → E
s : Finset ι
⊢ fourierInv.{u_3, u_4} (E := E) (∑ i ∈ s, f i) = ∑ i ∈ s, 𝓕⁻ (f i)

Tactic:
map_sum (AddMonoidHom.mk' 𝓕⁻ fourierInv_add) f s

Premises used: FourierInvAdd.fourierInv_add, map_sum, FourierTransformInv.fourierInv, AddMonoidHom.mk'
-- Module: Mathlib.Analysis.Fourier.Notation
Goal:
R : Type u_2
E : Type u_3
F : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : FourierTransform E F
inst_6 : FourierAdd E F
inst_7 : FourierSMul R E F
f : E
⊢ (fourierₗ R E : (a : E) → F) f = 𝓕 f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Fourier.Notation
Goal:
R : Type u_2
E : Type u_3
F : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : FourierTransform E F
inst_6 : FourierAdd E F
inst_7 : FourierSMul R E F
inst_8 : TopologicalSpace E
inst_9 : TopologicalSpace F
inst_10 : ContinuousFourier E F
f : E
⊢ (fourierCLM R E : (a : E) → F) f = 𝓕 f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Fourier.Notation
Goal:
R : Type u_2
E : Type u_3
F : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : FourierTransformInv E F
inst_6 : FourierInvAdd E F
inst_7 : FourierInvSMul R E F
f : E
⊢ (fourierInvₗ R E : (a : E) → F) f = 𝓕⁻ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Fourier.Notation
Goal:
R : Type u_2
E : Type u_3
F : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : FourierTransformInv E F
inst_6 : FourierInvAdd E F
inst_7 : FourierInvSMul R E F
inst_8 : TopologicalSpace E
inst_9 : TopologicalSpace F
inst_10 : ContinuousFourierInv E F
f : E
⊢ (fourierInvCLM R E : (a : E) → F) f = 𝓕⁻ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Fourier.Notation
Goal:
R : Type u_5
E : Type u_6
F : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : FourierTransform E F
inst_6 : FourierAdd E F
inst_7 : FourierSMul R E F
inst_8 : FourierTransformInv F E
inst_9 : FourierPair E F
inst_10 : FourierInvPair F E
f : E
⊢ (fourierEquiv R E : (a : E) → F) f = 𝓕 f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Fourier.Notation
Goal:
R : Type u_5
E : Type u_6
F : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : FourierTransform E F
inst_6 : FourierAdd E F
inst_7 : FourierSMul R E F
inst_8 : FourierTransformInv F E
inst_9 : FourierPair E F
inst_10 : FourierInvPair F E
f : F
⊢ (LinearEquiv.symm (fourierEquiv R E) : (a : F) → E) f = 𝓕⁻ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Fourier.Notation
Goal:
R : Type u_5
E : Type u_6
F : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : FourierTransform E F
inst_6 : FourierAdd E F
inst_7 : FourierSMul R E F
inst_8 : FourierTransformInv F E
inst_9 : FourierPair E F
inst_10 : FourierInvPair F E
inst_11 : TopologicalSpace E
inst_12 : TopologicalSpace F
inst_13 : ContinuousFourier E F
inst_14 : ContinuousFourierInv F E
f : E
⊢ (fourierCLE R E : (a : E) → F) f = 𝓕 f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Fourier.Notation
Goal:
R : Type u_5
E : Type u_6
F : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module R E
inst_4 : Module R F
inst_5 : FourierTransform E F
inst_6 : FourierAdd E F
inst_7 : FourierSMul R E F
inst_8 : FourierTransformInv F E
inst_9 : FourierPair E F
inst_10 : FourierInvPair F E
inst_11 : TopologicalSpace E
inst_12 : TopologicalSpace F
inst_13 : ContinuousFourier E F
inst_14 : ContinuousFourierInv F E
f : F
⊢ (ContinuousLinearEquiv.symm (fourierCLE R E) : (a : F) → E) f = 𝓕⁻ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
⊢ ∀ (x : ℝ), Norm.norm (E := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ) = 1

Tactic:
have (x : ℝ) : ‖e x‖ = 1 := (AddCircle.toCircle (-m • x)).norm_coe
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
this : ∀ (x : ℝ), Norm.norm (E := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ) = 1
K : Compacts ℝ
g : C(ℝ, ℂ)
simp_rw :
  Eq (α := ℝ)
    (⨆ (x : (↑(↑K : Set ℝ) : Type)),
      Norm.norm (E := ℂ) ((ContinuousMap.restrict (↑K : Set ℝ) (e * g) : (a : (↑(↑K : Set ℝ) : Type)) → ℂ) x : ℂ))
    (⨆ (x : (↑(↑K : Set ℝ) : Type)),
      Norm.norm (E := ℂ) ((ContinuousMap.restrict (↑K : Set ℝ) g : (a : (↑(↑K : Set ℝ) : Type)) → ℂ) x : ℂ))
simp_rw₁ :
  Eq (α := ℝ) (⨆ (x : (↑(↑K : Set ℝ) : Type)), Norm.norm (E := ℂ) ((e * g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
    (⨆ (x : (↑(↑K : Set ℝ) : Type)), Norm.norm (E := ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
simp_rw₂ :
  Eq (α := ℝ)
    (⨆ (x : (↑(↑K : Set ℝ) : Type)),
      ‖HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ)‖)
    (⨆ (x : (↑(↑K : Set ℝ) : Type)), Norm.norm (E := ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
simp_rw₃ :
  Eq (α := ℝ)
    (⨆ (x : (↑(↑K : Set ℝ) : Type)),
      Norm.norm (E := ℂ) ((e : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ) * Norm.norm (E := ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
    (⨆ (x : (↑(↑K : Set ℝ) : Type)), Norm.norm (E := ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
simp_rw₄ :
  Eq (α := ℝ) (⨆ (x : (↑(↑K : Set ℝ) : Type)), 1 * Norm.norm (E := ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
    (⨆ (x : (↑(↑K : Set ℝ) : Type)), Norm.norm (E := ℂ) ((g : (a : ℝ) → ℂ) (↑x : ℝ) : ℂ))
⊢ ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖

Tactic:
simp_rw [norm_eq_iSup_norm, restrict_apply, mul_apply, norm_mul, this, one_mul]

Premises used: ContinuousMap.norm_eq_iSup_norm, norm_mul, ContinuousMap.mul_apply, one_mul, ContinuousMap.restrict_apply
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
⊢ ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖

Tactic:
have neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖(e * g).restrict K‖ = ‖g.restrict K‖ := by
    have (x : ℝ) : ‖e x‖ = 1 := (AddCircle.toCircle (-m • x)).norm_coe
    intro K g
    simp_rw [norm_eq_iSup_norm, restrict_apply, mul_apply, norm_mul, this, one_mul]
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK :
  ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
n : ℤ
h : ∀ (x : ℝ), Eq (α := ℂ) ((e.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
⊢ e.comp (ContinuousMap.addRight (↑n : ℝ)) = e

Tactic:
ext1 x
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK :
  ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
n : ℤ
x : ℝ
⊢ Periodic (α := ℝ) (β := ℂ) (⇑e : (a : ℝ) → ℂ) 1

Tactic:
have : Periodic e 1 := Periodic.comp (fun x => AddCircle.coe_add_period 1 x) (fourier (-m))
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK :
  ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
n : ℤ
x : ℝ
this : Periodic (α := ℝ) (β := ℂ) (⇑e : (a : ℝ) → ℂ) 1
⊢ Eq (α := ℂ) ((e.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)

Tactic:
simpa only [mul_one] using this.int_mul n x

Premises used: Function.Periodic.int_mul, mul_one
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK :
  ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
⊢ ∀ (n : ℤ), e.comp (ContinuousMap.addRight (↑n : ℝ)) = e

Tactic:
have eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight n) = e := by
    intro n; ext1 x
    have : Periodic e 1 := Periodic.comp (fun x => AddCircle.coe_add_period 1 x) (fourier (-m))
    simpa only [mul_one] using this.int_mul n x
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK :
  ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight (↑n : ℝ)) = e
simp_rw :
  Eq (α := ℂ)
    (∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
    (∫ (x : ℝ) in 0..1,
      ∑' (n : ℤ),
        HMul.hMul (α := (a : ℝ) → ℂ) (β := (a : ℝ) → ℂ) (⇑e : (a : ℝ) → ℂ)
          (⇑(f.comp (ContinuousMap.addRight (↑n : ℝ))) : (a : ℝ) → ℂ) x)
simp_rw₁ :
  Eq (α := ℂ)
    (∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
    (∫ (x : ℝ) in 0..1,
      ∑' (n : ℤ),
        HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
          ((f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
simp_rw₂ :
  Eq (α := ℂ)
    (∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        (∑' (i : ℤ), (f.comp (ContinuousMap.addRight (↑i : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
    (∫ (x : ℝ) in 0..1,
      ∑' (n : ℤ),
        HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
          ((f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
⊢ Eq (α := ℂ)
    (∫ (x : ℝ) in 0..1,
      HMul.hMul (α := ℂ) (β := ℂ) ((e : (a : ℝ) → ℂ) x : ℂ)
        ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x : ℂ))
    (∫ (x : ℝ) in 0..1, ∑' (n : ℤ), (e * f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x)

Tactic:
simp_rw [coe_mul, Pi.mul_apply,
        ← ContinuousMap.tsum_apply (summable_of_locally_summable_norm hf), tsum_mul_left]

Premises used: Pi.mul_apply, ContinuousMap.summable_of_locally_summable_norm, tsum_mul_left, ContinuousMap.tsum_apply, ContinuousMap.coe_mul
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
m : ℤ
e : C(ℝ, ℂ) :=
  ContinuousMap.comp (β := AddCircle (𝕜 := ℝ) 1) (fourier (-m)) { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK :
  ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (e * g)‖ = ‖ContinuousMap.restrict (↑K : Set ℝ) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight (↑n : ℝ)) = e
⊢ Eq (α := ℂ) (∫ (x : ℝ) in 0..1, ∑' (n : ℤ), (e * f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x)
    (∑' (n : ℤ), ∫ (x : ℝ) in 0..1, (e * f.comp (ContinuousMap.addRight (↑n : ℝ)) : (a : ℝ) → ℂ) x)

Tactic:
(intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm ?_).symm

Premises used: intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm, Eq.symm