internlm/Lean-Github huggingface dataset:
Theorem: closeSmoothApproxPeriodic
Proof state before:
case intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
⊢ ∃ f₀, ContDiff ℝ ⊤ f₀ ∧ Function.Periodic f₀ (2 * Real.pi) ∧ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε
Tactic:
set f₀ := MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume with f₀def
Proof state after:
case intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ∃ f₀, ContDiff ℝ ⊤ f₀ ∧ Function.Periodic f₀ (2 * Real.pi) ∧ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε
Theorem: closeSmoothApproxPeriodic
Proof state before:
case intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ∃ f₀, ContDiff ℝ ⊤ f₀ ∧ Function.Periodic f₀ (2 * Real.pi) ∧ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε
Tactic:
use f₀
Proof state after:
case h
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ContDiff ℝ ⊤ f₀ ∧ Function.Periodic f₀ (2 * Real.pi) ∧ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε
Theorem: closeSmoothApproxPeriodic
Proof state before:
case h
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ContDiff ℝ ⊤ f₀ ∧ Function.Periodic f₀ (2 * Real.pi) ∧ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε
Tactic:
constructor
Proof state after:
case h.left
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ContDiff ℝ ⊤ f₀

case h.right
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ Function.Periodic f₀ (2 * Real.pi) ∧ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε
Theorem: closeSmoothApproxPeriodic
Proof state before:
case h.left
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ContDiff ℝ ⊤ f₀

case h.right
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ Function.Periodic f₀ (2 * Real.pi) ∧ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε
Tactic:
. 
  apply HasCompactSupport.contDiff_convolution_left
  . exact ContDiffBump.hasCompactSupport_normed φ
  . exact ContDiffBump.contDiff_normed φ
  . refine Continuous.locallyIntegrable ?h.left.hg.hf
    exact unicontf.continuous
Proof state after:
case h.right
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ Function.Periodic f₀ (2 * Real.pi) ∧ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε
Theorem: closeSmoothApproxPeriodic
Proof state before:
case h.right
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ Function.Periodic f₀ (2 * Real.pi) ∧ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε
Tactic:
constructor
Proof state after:
case h.right.left
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ Function.Periodic f₀ (2 * Real.pi)

case h.right.right
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε
Theorem: closeSmoothApproxPeriodic
Proof state before:
case h.right.left
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ Function.Periodic f₀ (2 * Real.pi)

case h.right.right
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε
Tactic:
. 
  intro x
  rw [f₀def, MeasureTheory.convolution, MeasureTheory.convolution]
  congr
  ext t
  congr 1
  convert periodicf (x - t) using 2
  ring
Proof state after:
case h.right.right
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε
Theorem: closeSmoothApproxPeriodic
Proof state before:
case h.right.right
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε
Tactic:
. intro x
  rw [← Complex.dist_eq, dist_comm]
  apply ContDiffBump.dist_normed_convolution_le
  . exact unicontf.continuous.aestronglyMeasurable
  . intro y hy
    simp only [Metric.mem_ball] at hy
    exact (hδ hy).le
Proof state after:
no goals
Theorem: closeSmoothApproxPeriodic
Proof state before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
⊢ 0 < δ / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: closeSmoothApproxPeriodic
Proof state before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
⊢ δ / 2 < δ
Tactic:
linarith
Proof state after:
no goals
Theorem: closeSmoothApproxPeriodic
Proof state before:
case h.left
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ContDiff ℝ ⊤ f₀
Tactic:
apply HasCompactSupport.contDiff_convolution_left
Proof state after:
case h.left.hcf
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ HasCompactSupport (φ.normed MeasureTheory.volume)

case h.left.hf
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ContDiff ℝ ⊤ (φ.normed MeasureTheory.volume)

case h.left.hg
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ MeasureTheory.LocallyIntegrable f MeasureTheory.volume
Theorem: closeSmoothApproxPeriodic
Proof state before:
case h.left.hcf
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ HasCompactSupport (φ.normed MeasureTheory.volume)

case h.left.hf
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ContDiff ℝ ⊤ (φ.normed MeasureTheory.volume)

case h.left.hg
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ MeasureTheory.LocallyIntegrable f MeasureTheory.volume
Tactic:
. exact ContDiffBump.hasCompactSupport_normed φ
Proof state after:
case h.left.hf
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ContDiff ℝ ⊤ (φ.normed MeasureTheory.volume)

case h.left.hg
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ MeasureTheory.LocallyIntegrable f MeasureTheory.volume
Theorem: closeSmoothApproxPeriodic
Proof state before:
case h.left.hf
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ContDiff ℝ ⊤ (φ.normed MeasureTheory.volume)

case h.left.hg
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ MeasureTheory.LocallyIntegrable f MeasureTheory.volume
Tactic:
. exact ContDiffBump.contDiff_normed φ
Proof state after:
case h.left.hg
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ MeasureTheory.LocallyIntegrable f MeasureTheory.volume
Theorem: closeSmoothApproxPeriodic
Proof state before:
case h.left.hg
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ MeasureTheory.LocallyIntegrable f MeasureTheory.volume
Tactic:
. refine Continuous.locallyIntegrable ?h.left.hg.hf
  exact unicontf.continuous
Proof state after:
no goals
Theorem: closeSmoothApproxPeriodic
Proof state before:
case h.left.hcf
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ HasCompactSupport (φ.normed MeasureTheory.volume)
Tactic:
exact ContDiffBump.hasCompactSupport_normed φ
Proof state after:
no goals
Theorem: closeSmoothApproxPeriodic
Proof state before:
case h.left.hf
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ContDiff ℝ ⊤ (φ.normed MeasureTheory.volume)
Tactic:
exact ContDiffBump.contDiff_normed φ
Proof state after:
no goals
Theorem: closeSmoothApproxPeriodic
Proof state before:
case h.left.hg
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ MeasureTheory.LocallyIntegrable f MeasureTheory.volume
Tactic:
refine Continuous.locallyIntegrable ?h.left.hg.hf
Proof state after:
case h.left.hg.hf
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ Continuous f
Theorem: closeSmoothApproxPeriodic
Proof state before:
case h.left.hg.hf
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
φ : ContDiffBump 0 := { rIn := δ / 2, rOut := δ, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f₀ : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
f₀def :
  f₀ = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ Continuous f
Tactic:
exact unicontf.continuous
Proof state after:
no goals