internlm/Lean-Github huggingface dataset:
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)
Tactic:
intro x
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
x : ℝ
⊢ f₀ (x + 2 * Real.pi) = 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
x : ℝ
⊢ f₀ (x + 2 * Real.pi) = f₀ x
Tactic:
rw [f₀def, MeasureTheory.convolution, MeasureTheory.convolution]
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
x : ℝ
⊢ ∫ (t : ℝ), ((ContinuousLinearMap.lsmul ℝ ℝ) (φ.normed MeasureTheory.volume t)) (f (x + 2 * Real.pi - t)) =
    ∫ (t : ℝ), ((ContinuousLinearMap.lsmul ℝ ℝ) (φ.normed MeasureTheory.volume t)) (f (x - t))
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
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
Proof 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))
Theorem: closeSmoothApproxPeriodic
Proof 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
Proof 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))
Theorem: closeSmoothApproxPeriodic
Proof 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
Proof 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)
Theorem: closeSmoothApproxPeriodic
Proof 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
Proof 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
Theorem: closeSmoothApproxPeriodic
Proof 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
Proof state after:
no goals
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
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:
rw [← Complex.dist_eq, dist_comm]
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 : ℝ
⊢ dist (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 : ℝ
⊢ dist (f₀ x) (f x) ≤ ε
Tactic:
apply ContDiffBump.dist_normed_convolution_le
Proof 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) ≤ ε
Theorem: closeSmoothApproxPeriodic
Proof 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
Proof 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) ≤ ε
Theorem: closeSmoothApproxPeriodic
Proof 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
Proof state after:
no goals
Theorem: closeSmoothApproxPeriodic
Proof 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
Proof state after:
no goals
Theorem: closeSmoothApproxPeriodic
Proof 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
Proof 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) ≤ ε
Theorem: closeSmoothApproxPeriodic
Proof 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
Proof 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) ≤ ε
Theorem: closeSmoothApproxPeriodic
Proof 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
Proof state after:
no goals
Theorem: Real.summable_of_le
Proof state before:
β : Type
f g : β → ℝ
hgpos : 0 ≤ g
hgf : ∀ (b : β), g b ≤ f b
summablef : Summable f
⊢ Summable g
Tactic:
exact Summable.of_nonneg_of_le hgpos hgf summablef
Proof state after:
no goals
Theorem: summable_of_le_on_nonzero
Proof state before:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
⊢ Summable g
Tactic:
set f' : ℤ → ℝ := fun i ↦ if i = 0 then g i else f i with f'def
Proof state after:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
⊢ Summable g
Theorem: summable_of_le_on_nonzero
Proof state before:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
⊢ Summable g
Tactic:
have : ∀ i, g i ≤ f' i := by
  intro i
  rw [f'def]
  by_cases h : i = 0
  . simp [h]
  . simp only [h, ↓reduceIte]
    exact hgf i h
Proof state after:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
this : ∀ (i : ℤ), g i ≤ f' i
⊢ Summable g
Theorem: summable_of_le_on_nonzero
Proof state before:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
this : ∀ (i : ℤ), g i ≤ f' i
⊢ Summable g
Tactic:
apply Real.summable_of_le hgpos this
Proof state after:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
this : ∀ (i : ℤ), g i ≤ f' i
⊢ Summable fun b => f' b
Theorem: summable_of_le_on_nonzero
Proof state before:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
this : ∀ (i : ℤ), g i ≤ f' i
⊢ Summable fun b => f' b
Tactic:
let s : Finset ℤ := {0}
Proof state after:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
this : ∀ (i : ℤ), g i ≤ f' i
s : Finset ℤ := {0}
⊢ Summable fun b => f' b
Theorem: summable_of_le_on_nonzero
Proof state before:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
this : ∀ (i : ℤ), g i ≤ f' i
s : Finset ℤ := {0}
⊢ Summable fun b => f' b
Tactic:
rw [←s.summable_compl_iff]
Proof state after:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
this : ∀ (i : ℤ), g i ≤ f' i
s : Finset ℤ := {0}
⊢ Summable fun x => f' ↑x
Theorem: summable_of_le_on_nonzero
Proof state before:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
this : ∀ (i : ℤ), g i ≤ f' i
s : Finset ℤ := {0}
⊢ Summable fun x => f' ↑x
Tactic:
apply (summable_congr _).mpr (s.summable_compl_iff.mpr summablef)
Proof state after:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
this : ∀ (i : ℤ), g i ≤ f' i
s : Finset ℤ := {0}
⊢ ∀ (b : { x // x ∉ s }), f' ↑b = f ↑b