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

State before:
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
εpos : ε > 0
⊢ ∃ f₀, ContDiff ℝ ⊤ f₀ ∧ ∀ (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
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
⊢ ∃ f₀, ContDiff ℝ ⊤ f₀ ∧ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε

State before:
case intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
⊢ ∃ f₀, ContDiff ℝ ⊤ f₀ ∧ ∀ (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
ε : ℝ
ε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₀ ∧ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε

State before:
case intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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₀ ∧ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε
Tactic:
let f_0 := MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
State after:
case intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ∃ f₀, ContDiff ℝ ⊤ f₀ ∧ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε

State before:
case intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ∃ f₀, ContDiff ℝ ⊤ f₀ ∧ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε
Tactic:
use f_0
State after:
case h
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ContDiff ℝ ⊤ f_0 ∧ ∀ (x : ℝ), Complex.abs (f x - f_0 x) ≤ ε

State before:
case h
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ContDiff ℝ ⊤ f_0 ∧ ∀ (x : ℝ), Complex.abs (f x - f_0 x) ≤ ε
Tactic:
constructor
State after:
case h.left
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ContDiff ℝ ⊤ f_0

case h.right
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ∀ (x : ℝ), Complex.abs (f x - f_0 x) ≤ ε

State before:
case h.left
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ContDiff ℝ ⊤ f_0

case h.right
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ∀ (x : ℝ), Complex.abs (f x - f_0 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
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ∀ (x : ℝ), Complex.abs (f x - f_0 x) ≤ ε

State before:
case h.right
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ∀ (x : ℝ), Complex.abs (f x - f_0 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
ε : ℝ
ε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
ε : ℝ
ε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
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ContDiff ℝ ⊤ f_0
Tactic:
apply HasCompactSupport.contDiff_convolution_left
State after:
case h.left.hcf
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ HasCompactSupport (φ.normed MeasureTheory.volume)

case h.left.hf
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ContDiff ℝ ⊤ (φ.normed MeasureTheory.volume)

case h.left.hg
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  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
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ HasCompactSupport (φ.normed MeasureTheory.volume)

case h.left.hf
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ContDiff ℝ ⊤ (φ.normed MeasureTheory.volume)

case h.left.hg
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  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
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ContDiff ℝ ⊤ (φ.normed MeasureTheory.volume)

case h.left.hg
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  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
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ContDiff ℝ ⊤ (φ.normed MeasureTheory.volume)

case h.left.hg
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  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
ε : ℝ
ε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_0 : ℝ → ℂ :=
  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
ε : ℝ
ε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_0 : ℝ → ℂ :=
  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
ε : ℝ
ε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_0 : ℝ → ℂ :=
  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
ε : ℝ
ε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_0 : ℝ → ℂ :=
  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
ε : ℝ
ε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_0 : ℝ → ℂ :=
  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
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ Continuous f

State before:
case h.left.hg.hf
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  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
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
⊢ ∀ (x : ℝ), Complex.abs (f x - f_0 x) ≤ ε
Tactic:
intro x
State after:
case h.right
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
x : ℝ
⊢ Complex.abs (f x - f_0 x) ≤ ε

State before:
case h.right
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
x : ℝ
⊢ Complex.abs (f x - f_0 x) ≤ ε
Tactic:
rw [← Complex.dist_eq, dist_comm]
State after:
case h.right
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
x : ℝ
⊢ dist (f_0 x) (f x) ≤ ε

State before:
case h.right
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
x : ℝ
⊢ dist (f_0 x) (f x) ≤ ε
Tactic:
apply ContDiffBump.dist_normed_convolution_le
State after:
case h.right.hmg
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
x : ℝ
⊢ MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume

case h.right.hg
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  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.hmg
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume
x : ℝ
⊢ MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume

case h.right.hg
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  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.hg
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  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.hg
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  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.hmg
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  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.hg
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  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.hg
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  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.hg
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  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.hg
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  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.hg
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
ε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_0 : ℝ → ℂ :=
  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