Theorem: closeSmoothApproxPeriodic (Carleson/Theorem1_1/Approximation.lean)

State before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : ε > 0
⊢ ∃ f₀, ContDiff ℝ ⊤ f₀ ∧ Function.Periodic f₀ (2 * Real.pi) ∧ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε
Tactic:
obtain ⟨δ, δpos, hδ⟩ := (Metric.uniformContinuous_iff.mp unicontf) ε εpos
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) < ε
⊢ ∃ f₀, ContDiff ℝ ⊤ f₀ ∧ Function.Periodic f₀ (2 * Real.pi) ∧ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε

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) < ε
⊢ ∃ f₀, ContDiff ℝ ⊤ f₀ ∧ Function.Periodic f₀ (2 * Real.pi) ∧ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε
Tactic:
let φ : ContDiffBump (0 : ℝ) := ⟨δ/2, δ, by linarith, by linarith⟩
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₀, ContDiff ℝ ⊤ f₀ ∧ Function.Periodic f₀ (2 * Real.pi) ∧ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε

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
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) ≤ ε

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₀
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) ≤ ε

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
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) ≤ ε

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
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) ≤ ε

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
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) ≤ ε

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
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) ≤ ε

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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

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 φ
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

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 φ
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

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
State after:
no goals

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 φ
State after:
no goals

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 φ
State after:
no goals

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
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

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
State after:
no goals

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)
Tactic:
intro x
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
x : ℝ
⊢ f₀ (x + 2 * Real.pi) = f₀ x

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
x : ℝ
⊢ f₀ (x + 2 * Real.pi) = f₀ x
Tactic:
rw [f₀def, MeasureTheory.convolution, MeasureTheory.convolution]
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
x : ℝ
⊢ ∫ (t : ℝ), ((ContinuousLinearMap.lsmul ℝ ℝ) (φ.normed MeasureTheory.volume t)) (f (x + 2 * Real.pi - t)) =
    ∫ (t : ℝ), ((ContinuousLinearMap.lsmul ℝ ℝ) (φ.normed MeasureTheory.volume t)) (f (x - t))

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
x : ℝ
⊢ ∫ (t : ℝ), ((ContinuousLinearMap.lsmul ℝ ℝ) (φ.normed MeasureTheory.volume t)) (f (x + 2 * Real.pi - t)) =
    ∫ (t : ℝ), ((ContinuousLinearMap.lsmul ℝ ℝ) (φ.normed MeasureTheory.volume t)) (f (x - t))
Tactic:
congr
State after:
case h.right.left.e_f
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 : ℝ
⊢ (fun t => ((ContinuousLinearMap.lsmul ℝ ℝ) (φ.normed MeasureTheory.volume t)) (f (x + 2 * Real.pi - t))) = fun t =>
    ((ContinuousLinearMap.lsmul ℝ ℝ) (φ.normed MeasureTheory.volume t)) (f (x - t))

State before:
case h.right.left.e_f
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 : ℝ
⊢ (fun t => ((ContinuousLinearMap.lsmul ℝ ℝ) (φ.normed MeasureTheory.volume t)) (f (x + 2 * Real.pi - t))) = fun t =>
    ((ContinuousLinearMap.lsmul ℝ ℝ) (φ.normed MeasureTheory.volume t)) (f (x - t))
Tactic:
ext t
State after:
case h.right.left.e_f.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
x t : ℝ
⊢ ((ContinuousLinearMap.lsmul ℝ ℝ) (φ.normed MeasureTheory.volume t)) (f (x + 2 * Real.pi - t)) =
    ((ContinuousLinearMap.lsmul ℝ ℝ) (φ.normed MeasureTheory.volume t)) (f (x - t))

State before:
case h.right.left.e_f.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
x t : ℝ
⊢ ((ContinuousLinearMap.lsmul ℝ ℝ) (φ.normed MeasureTheory.volume t)) (f (x + 2 * Real.pi - t)) =
    ((ContinuousLinearMap.lsmul ℝ ℝ) (φ.normed MeasureTheory.volume t)) (f (x - t))
Tactic:
congr 1
State after:
case h.right.left.e_f.h.h.e_6.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
x t : ℝ
⊢ f (x + 2 * Real.pi - t) = f (x - t)

State before:
case h.right.left.e_f.h.h.e_6.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
x t : ℝ
⊢ f (x + 2 * Real.pi - t) = f (x - t)
Tactic:
convert periodicf (x - t) using 2
State after:
case h.e'_2.h.e'_1
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 t : ℝ
⊢ x + 2 * Real.pi - t = x - t + 2 * Real.pi

State before:
case h.e'_2.h.e'_1
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 t : ℝ
⊢ x + 2 * Real.pi - t = x - t + 2 * Real.pi
Tactic:
ring
State after:
no goals

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
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) ≤ ε

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:
rw [← Complex.dist_eq, dist_comm]
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 : ℝ
⊢ dist (f₀ x) (f x) ≤ ε

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 : ℝ
⊢ dist (f₀ x) (f x) ≤ ε
Tactic:
apply ContDiffBump.dist_normed_convolution_le
State after:
case h.right.right.hmg
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 : ℝ
⊢ MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume

case h.right.right.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
x : ℝ
⊢ ∀ x_1 ∈ Metric.ball x φ.rOut, dist (f x_1) (f x) ≤ ε

State before:
case h.right.right.hmg
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 : ℝ
⊢ MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume

case h.right.right.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
x : ℝ
⊢ ∀ x_1 ∈ Metric.ball x φ.rOut, dist (f x_1) (f x) ≤ ε
Tactic:
. exact unicontf.continuous.aestronglyMeasurable
State after:
case h.right.right.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
x : ℝ
⊢ ∀ x_1 ∈ Metric.ball x φ.rOut, dist (f x_1) (f x) ≤ ε

State before:
case h.right.right.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
x : ℝ
⊢ ∀ x_1 ∈ Metric.ball x φ.rOut, dist (f x_1) (f x) ≤ ε
Tactic:
. intro y hy
  simp only [Metric.mem_ball] at hy
  exact (hδ hy).le
State after:
no goals

State before:
case h.right.right.hmg
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 : ℝ
⊢ MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume
Tactic:
exact unicontf.continuous.aestronglyMeasurable
State after:
no goals

State before:
case h.right.right.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
x : ℝ
⊢ ∀ x_1 ∈ Metric.ball x φ.rOut, dist (f x_1) (f x) ≤ ε
Tactic:
intro y hy
State after:
case h.right.right.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
x y : ℝ
hy : y ∈ Metric.ball x φ.rOut
⊢ dist (f y) (f x) ≤ ε

State before:
case h.right.right.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
x y : ℝ
hy : y ∈ Metric.ball x φ.rOut
⊢ dist (f y) (f x) ≤ ε
Tactic:
simp only [Metric.mem_ball] at hy
State after:
case h.right.right.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
x y : ℝ
hy : dist y x < δ
⊢ dist (f y) (f x) ≤ ε

State before:
case h.right.right.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
x y : ℝ
hy : dist y x < δ
⊢ dist (f y) (f x) ≤ ε
Tactic:
exact (hδ hy).le
State after:
no goals