[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
⊢ fourierCoeff (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
      m =
    𝓕 ↑f ↑m
[PROOFSTEP]
let e : C(ℝ, ℂ) := (fourier (-m)).comp ⟨((↑) : ℝ → UnitAddCircle), continuous_quotient_mk'⟩
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
⊢ fourierCoeff (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
      m =
    𝓕 ↑f ↑m
[PROOFSTEP]
have neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖(e * g).restrict K‖ = ‖g.restrict K‖ :=
  by
  have : ∀ x : ℝ, ‖e x‖ = 1 := fun x => abs_coe_circle (AddCircle.toCircle (-m • x))
  intro K g
  simp_rw [norm_eq_iSup_norm, restrict_apply, mul_apply, norm_mul, this, one_mul]
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
⊢ ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
[PROOFSTEP]
have : ∀ x : ℝ, ‖e x‖ = 1 := fun x => abs_coe_circle (AddCircle.toCircle (-m • x))
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
this : ∀ (x : ℝ), ‖↑e x‖ = 1
⊢ ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
[PROOFSTEP]
intro K g
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
this : ∀ (x : ℝ), ‖↑e x‖ = 1
K : Compacts ℝ
g : C(ℝ, ℂ)
⊢ ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
[PROOFSTEP]
simp_rw [norm_eq_iSup_norm, restrict_apply, mul_apply, norm_mul, this, one_mul]
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
⊢ fourierCoeff (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
      m =
    𝓕 ↑f ↑m
[PROOFSTEP]
have eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight n) = e :=
  by
  intro n; ext1 x
  have : Periodic e 1 := Periodic.comp (fun x => AddCircle.coe_add_period 1 x) (fourier (-m))
  simpa only [mul_one] using this.int_mul n x
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
⊢ ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
[PROOFSTEP]
intro n
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
n : ℤ
⊢ ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
[PROOFSTEP]
ext1 x
[GOAL]
case h
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
n : ℤ
x : ℝ
⊢ ↑(ContinuousMap.comp e (ContinuousMap.addRight ↑n)) x = ↑e x
[PROOFSTEP]
have : Periodic e 1 := Periodic.comp (fun x => AddCircle.coe_add_period 1 x) (fourier (-m))
[GOAL]
case h
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
n : ℤ
x : ℝ
this : Periodic (↑e) 1
⊢ ↑(ContinuousMap.comp e (ContinuousMap.addRight ↑n)) x = ↑e x
[PROOFSTEP]
simpa only [mul_one] using this.int_mul n x
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ fourierCoeff (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
      m =
    𝓕 ↑f ↑m
[PROOFSTEP]
calc
  fourierCoeff (Periodic.lift <| f.periodic_tsum_comp_add_zsmul 1) m =
      ∫ x in (0 : ℝ)..1, e x * (∑' n : ℤ, f.comp (ContinuousMap.addRight n)) x :=
    by
    simp_rw [fourierCoeff_eq_intervalIntegral _ m 0, div_one, one_smul, zero_add, comp_apply, coe_mk, Periodic.lift_coe,
      zsmul_one, smul_eq_mul]
      -- Transform sum in C(ℝ, ℂ) evaluated at x into pointwise sum of values.
  _ = ∫ x in (0 : ℝ)..1, ∑' n : ℤ, (e * f.comp (ContinuousMap.addRight n)) x := by
    simp_rw [coe_mul, Pi.mul_apply, ← ContinuousMap.tsum_apply (summable_of_locally_summable_norm hf), tsum_mul_left]
      -- Swap sum and integral.
  _ = ∑' n : ℤ, ∫ x in (0 : ℝ)..1, (e * f.comp (ContinuousMap.addRight n)) x :=
    by
    refine' (intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm _).symm
    convert hf ⟨uIcc 0 1, isCompact_uIcc⟩ using 1
    exact funext fun n => neK _ _
  _ = ∑' n : ℤ, ∫ x in (0 : ℝ)..1, (e * f).comp (ContinuousMap.addRight n) x :=
    by
    simp only [ContinuousMap.comp_apply, mul_comp] at eadd ⊢
    simp_rw [eadd]
      -- Rearrange sum of interval integrals into an integral over `ℝ`.
  _ = ∫ x, e x * f x :=
    by
    suffices Integrable (e * f) from this.hasSum_intervalIntegral_comp_add_int.tsum_eq
    apply integrable_of_summable_norm_Icc
    convert hf ⟨Icc 0 1, isCompact_Icc⟩ using 1
    simp_rw [mul_comp] at eadd ⊢
    simp_rw [eadd]
    exact
      funext fun n =>
        neK ⟨Icc 0 1, isCompact_Icc⟩
          _
            -- Minor tidying to finish
  _ = 𝓕 f m := by
    rw [fourierIntegral_eq_integral_exp_smul]
    congr 1 with x : 1
    rw [smul_eq_mul, comp_apply, coe_mk, coe_mk, ContinuousMap.toFun_eq_coe, fourier_coe_apply]
    congr 2
    push_cast
    ring
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ fourierCoeff (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
      m =
    ∫ (x : ℝ) in 0 ..1, ↑e x * ↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight ↑n)) x
[PROOFSTEP]
simp_rw [fourierCoeff_eq_intervalIntegral _ m 0, div_one, one_smul, zero_add, comp_apply, coe_mk, Periodic.lift_coe,
  zsmul_one, smul_eq_mul]
  -- Transform sum in C(ℝ, ℂ) evaluated at x into pointwise sum of values.
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ ∫ (x : ℝ) in 0 ..1, ↑e x * ↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight ↑n)) x =
    ∫ (x : ℝ) in 0 ..1, ∑' (n : ℤ), ↑(e * ContinuousMap.comp f (ContinuousMap.addRight ↑n)) x
[PROOFSTEP]
simp_rw [coe_mul, Pi.mul_apply, ← ContinuousMap.tsum_apply (summable_of_locally_summable_norm hf), tsum_mul_left]
  -- Swap sum and integral.
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ ∫ (x : ℝ) in 0 ..1, ∑' (n : ℤ), ↑(e * ContinuousMap.comp f (ContinuousMap.addRight ↑n)) x =
    ∑' (n : ℤ), ∫ (x : ℝ) in 0 ..1, ↑(e * ContinuousMap.comp f (ContinuousMap.addRight ↑n)) x
[PROOFSTEP]
refine' (intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm _).symm
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ Summable fun i =>
    ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := (_ : IsCompact (uIcc 0 1)) })
        (e * ContinuousMap.comp f (ContinuousMap.addRight ↑i))‖
[PROOFSTEP]
convert hf ⟨uIcc 0 1, isCompact_uIcc⟩ using 1
[GOAL]
case h.e'_5
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ (fun i =>
      ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := (_ : IsCompact (uIcc 0 1)) })
          (e * ContinuousMap.comp f (ContinuousMap.addRight ↑i))‖) =
    fun n =>
    ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := (_ : IsCompact (uIcc 0 1)) })
        (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
[PROOFSTEP]
exact funext fun n => neK _ _
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ ∑' (n : ℤ), ∫ (x : ℝ) in 0 ..1, ↑(e * ContinuousMap.comp f (ContinuousMap.addRight ↑n)) x =
    ∑' (n : ℤ), ∫ (x : ℝ) in 0 ..1, ↑(ContinuousMap.comp (e * f) (ContinuousMap.addRight ↑n)) x
[PROOFSTEP]
simp only [ContinuousMap.comp_apply, mul_comp] at eadd ⊢
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd :
  ∀ (n : ℤ),
    ContinuousMap.comp (ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk))
        (ContinuousMap.addRight ↑n) =
      ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
⊢ ∑' (n : ℤ),
      ∫ (x : ℝ) in 0 ..1,
        ↑(ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk) *
              ContinuousMap.comp f (ContinuousMap.addRight ↑n))
          x =
    ∑' (n : ℤ),
      ∫ (x : ℝ) in 0 ..1,
        ↑(ContinuousMap.comp (ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk))
                (ContinuousMap.addRight ↑n) *
              ContinuousMap.comp f (ContinuousMap.addRight ↑n))
          x
[PROOFSTEP]
simp_rw [eadd]
  -- Rearrange sum of interval integrals into an integral over `ℝ`.
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ ∑' (n : ℤ), ∫ (x : ℝ) in 0 ..1, ↑(ContinuousMap.comp (e * f) (ContinuousMap.addRight ↑n)) x = ∫ (x : ℝ), ↑e x * ↑f x
[PROOFSTEP]
suffices Integrable (e * f) from this.hasSum_intervalIntegral_comp_add_int.tsum_eq
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ Integrable ↑(e * f)
[PROOFSTEP]
apply integrable_of_summable_norm_Icc
[GOAL]
case hf
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (ContinuousMap.comp (e * f) (ContinuousMap.addRight ↑n))‖
[PROOFSTEP]
convert hf ⟨Icc 0 1, isCompact_Icc⟩ using 1
[GOAL]
case h.e'_5
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ (fun n => ‖ContinuousMap.restrict (Icc 0 1) (ContinuousMap.comp (e * f) (ContinuousMap.addRight ↑n))‖) = fun n =>
    ‖ContinuousMap.restrict (↑{ carrier := Icc 0 1, isCompact' := (_ : IsCompact (Icc 0 1)) })
        (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
[PROOFSTEP]
simp_rw [mul_comp] at eadd ⊢
[GOAL]
case h.e'_5
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd :
  ∀ (n : ℤ),
    ContinuousMap.comp (ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk))
        (ContinuousMap.addRight ↑n) =
      ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
⊢ (fun n =>
      ‖ContinuousMap.restrict (Icc 0 1)
          (ContinuousMap.comp (ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk))
              (ContinuousMap.addRight ↑n) *
            ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖) =
    fun n =>
    ‖ContinuousMap.restrict (↑{ carrier := Icc 0 1, isCompact' := (_ : IsCompact (Icc 0 1)) })
        (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
[PROOFSTEP]
simp_rw [eadd]
[GOAL]
case h.e'_5
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd :
  ∀ (n : ℤ),
    ContinuousMap.comp (ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk))
        (ContinuousMap.addRight ↑n) =
      ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
⊢ (fun n =>
      ‖ContinuousMap.restrict (Icc 0 1)
          (ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk) *
            ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖) =
    fun n =>
    ‖ContinuousMap.restrict (↑{ carrier := Icc 0 1, isCompact' := (_ : IsCompact (Icc 0 1)) })
        (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
[PROOFSTEP]
exact
  funext fun n =>
    neK ⟨Icc 0 1, isCompact_Icc⟩
      _
        -- Minor tidying to finish
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ ∫ (x : ℝ), ↑e x * ↑f x = 𝓕 ↑f ↑m
[PROOFSTEP]
rw [fourierIntegral_eq_integral_exp_smul]
[GOAL]
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
⊢ ∫ (x : ℝ), ↑e x * ↑f x = ∫ (v : ℝ), Complex.exp (↑(-2 * π * v * ↑m) * I) • ↑f v
[PROOFSTEP]
congr 1 with x : 1
[GOAL]
case e_f.h
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
x : ℝ
⊢ ↑e x * ↑f x = Complex.exp (↑(-2 * π * x * ↑m) * I) • ↑f x
[PROOFSTEP]
rw [smul_eq_mul, comp_apply, coe_mk, coe_mk, ContinuousMap.toFun_eq_coe, fourier_coe_apply]
[GOAL]
case e_f.h
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
x : ℝ
⊢ Complex.exp (2 * ↑π * I * ↑(-m) * ↑x / ↑1) * ↑f x = Complex.exp (↑(-2 * π * x * ↑m) * I) * ↑f x
[PROOFSTEP]
congr 2
[GOAL]
case e_f.h.e_a.e_z
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
x : ℝ
⊢ 2 * ↑π * I * ↑(-m) * ↑x / ↑1 = ↑(-2 * π * x * ↑m) * I
[PROOFSTEP]
push_cast
[GOAL]
case e_f.h.e_a.e_z
f : C(ℝ, ℂ)
hf :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk QuotientAddGroup.mk)
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), ContinuousMap.comp e (ContinuousMap.addRight ↑n) = e
x : ℝ
⊢ 2 * ↑π * I * -↑m * ↑x / 1 = -2 * ↑π * ↑x * ↑m * I
[PROOFSTEP]
ring
[GOAL]
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n => 𝓕 ↑f ↑n
⊢ ∑' (n : ℤ), ↑f ↑n = ∑' (n : ℤ), 𝓕 ↑f ↑n
[PROOFSTEP]
let F : C(UnitAddCircle, ℂ) :=
  ⟨(f.periodic_tsum_comp_add_zsmul 1).lift, continuous_coinduced_dom.mpr (map_continuous _)⟩
[GOAL]
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n => 𝓕 ↑f ↑n
F : C(UnitAddCircle, ℂ) :=
  ContinuousMap.mk
    (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
⊢ ∑' (n : ℤ), ↑f ↑n = ∑' (n : ℤ), 𝓕 ↑f ↑n
[PROOFSTEP]
have : Summable (fourierCoeff F) := by
  convert h_sum
  exact Real.fourierCoeff_tsum_comp_add h_norm _
[GOAL]
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n => 𝓕 ↑f ↑n
F : C(UnitAddCircle, ℂ) :=
  ContinuousMap.mk
    (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
⊢ Summable (fourierCoeff ↑F)
[PROOFSTEP]
convert h_sum
[GOAL]
case h.e'_5.h
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n => 𝓕 ↑f ↑n
F : C(UnitAddCircle, ℂ) :=
  ContinuousMap.mk
    (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
x✝ : ℤ
⊢ fourierCoeff (↑F) x✝ = 𝓕 ↑f ↑x✝
[PROOFSTEP]
exact Real.fourierCoeff_tsum_comp_add h_norm _
[GOAL]
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n => 𝓕 ↑f ↑n
F : C(UnitAddCircle, ℂ) :=
  ContinuousMap.mk
    (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
this : Summable (fourierCoeff ↑F)
⊢ ∑' (n : ℤ), ↑f ↑n = ∑' (n : ℤ), 𝓕 ↑f ↑n
[PROOFSTEP]
convert (has_pointwise_sum_fourier_series_of_summable this 0).tsum_eq.symm using 1
[GOAL]
case h.e'_2
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n => 𝓕 ↑f ↑n
F : C(UnitAddCircle, ℂ) :=
  ContinuousMap.mk
    (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
this : Summable (fourierCoeff ↑F)
⊢ ∑' (n : ℤ), ↑f ↑n = ↑F 0
[PROOFSTEP]
have := (hasSum_apply (summable_of_locally_summable_norm h_norm).hasSum 0).tsum_eq
[GOAL]
case h.e'_2
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n => 𝓕 ↑f ↑n
F : C(UnitAddCircle, ℂ) :=
  ContinuousMap.mk
    (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
this✝ : Summable (fourierCoeff ↑F)
this :
  ∑' (b : ℤ), ↑(ContinuousMap.comp f (ContinuousMap.addRight ↑b)) 0 =
    ↑(∑' (b : ℤ), ContinuousMap.comp f (ContinuousMap.addRight ↑b)) 0
⊢ ∑' (n : ℤ), ↑f ↑n = ↑F 0
[PROOFSTEP]
simpa only [coe_mk, ← QuotientAddGroup.mk_zero, Periodic.lift_coe, zsmul_one, comp_apply, coe_addRight, zero_add] using
  this
[GOAL]
case h.e'_3
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n => 𝓕 ↑f ↑n
F : C(UnitAddCircle, ℂ) :=
  ContinuousMap.mk
    (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
this : Summable (fourierCoeff ↑F)
⊢ ∑' (n : ℤ), 𝓕 ↑f ↑n = ∑' (b : ℤ), fourierCoeff (↑F) b • ↑(fourier b) 0
[PROOFSTEP]
congr 1 with n : 1
[GOAL]
case h.e'_3.e_f.h
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n => 𝓕 ↑f ↑n
F : C(UnitAddCircle, ℂ) :=
  ContinuousMap.mk
    (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
this : Summable (fourierCoeff ↑F)
n : ℤ
⊢ 𝓕 ↑f ↑n = fourierCoeff (↑F) n • ↑(fourier n) 0
[PROOFSTEP]
rw [← Real.fourierCoeff_tsum_comp_add h_norm n, fourier_eval_zero, smul_eq_mul, mul_one]
[GOAL]
case h.e'_3.e_f.h
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n => 𝓕 ↑f ↑n
F : C(UnitAddCircle, ℂ) :=
  ContinuousMap.mk
    (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
this : Summable (fourierCoeff ↑F)
n : ℤ
⊢ fourierCoeff (Periodic.lift (_ : Periodic (↑(∑' (n : ℤ), ContinuousMap.comp f (ContinuousMap.addRight (n • 1)))) 1))
      n =
    fourierCoeff (↑F) n
[PROOFSTEP]
rfl
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
⊢ (fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atTop] fun x => |x| ^ (-b)
[PROOFSTEP]
have claim : ∀ x : ℝ, max 0 (-2 * R) < x → ∀ y : ℝ, x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b) :=
  by
  intro x hx y hy
  rw [max_lt_iff] at hx 
  have hxR : 0 < x + R := by
    rcases le_or_lt 0 R with (h | h)
    · exact add_pos_of_pos_of_nonneg hx.1 h
    · rw [← sub_lt_iff_lt_add, zero_sub]
      refine' lt_trans _ hx.2
      rwa [neg_mul, neg_lt_neg_iff, two_mul, add_lt_iff_neg_left]
  have hy' : 0 < y := hxR.trans_le hy
  have : y ^ (-b) ≤ (x + R) ^ (-b) :=
    by
    rw [rpow_neg hy'.le, rpow_neg hxR.le, inv_le_inv (rpow_pos_of_pos hy' _) (rpow_pos_of_pos hxR _)]
    exact rpow_le_rpow hxR.le hy hb.le
  refine' this.trans _
  rw [← mul_rpow one_half_pos.le hx.1.le, rpow_neg (mul_pos one_half_pos hx.1).le, rpow_neg hxR.le]
  refine' inv_le_inv_of_le (rpow_pos_of_pos (mul_pos one_half_pos hx.1) _) _
  exact rpow_le_rpow (mul_pos one_half_pos hx.1).le (by linarith) hb.le
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
⊢ ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
[PROOFSTEP]
intro x hx y hy
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : max 0 (-2 * R) < x
y : ℝ
hy : x + R ≤ y
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
[PROOFSTEP]
rw [max_lt_iff] at hx 
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
[PROOFSTEP]
have hxR : 0 < x + R := by
  rcases le_or_lt 0 R with (h | h)
  · exact add_pos_of_pos_of_nonneg hx.1 h
  · rw [← sub_lt_iff_lt_add, zero_sub]
    refine' lt_trans _ hx.2
    rwa [neg_mul, neg_lt_neg_iff, two_mul, add_lt_iff_neg_left]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
⊢ 0 < x + R
[PROOFSTEP]
rcases le_or_lt 0 R with (h | h)
[GOAL]
case inl
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
h : 0 ≤ R
⊢ 0 < x + R
[PROOFSTEP]
exact add_pos_of_pos_of_nonneg hx.1 h
[GOAL]
case inr
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
h : R < 0
⊢ 0 < x + R
[PROOFSTEP]
rw [← sub_lt_iff_lt_add, zero_sub]
[GOAL]
case inr
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
h : R < 0
⊢ -R < x
[PROOFSTEP]
refine' lt_trans _ hx.2
[GOAL]
case inr
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
h : R < 0
⊢ -R < -2 * R
[PROOFSTEP]
rwa [neg_mul, neg_lt_neg_iff, two_mul, add_lt_iff_neg_left]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
hxR : 0 < x + R
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
[PROOFSTEP]
have hy' : 0 < y := hxR.trans_le hy
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
hxR : 0 < x + R
hy' : 0 < y
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
[PROOFSTEP]
have : y ^ (-b) ≤ (x + R) ^ (-b) :=
  by
  rw [rpow_neg hy'.le, rpow_neg hxR.le, inv_le_inv (rpow_pos_of_pos hy' _) (rpow_pos_of_pos hxR _)]
  exact rpow_le_rpow hxR.le hy hb.le
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
hxR : 0 < x + R
hy' : 0 < y
⊢ y ^ (-b) ≤ (x + R) ^ (-b)
[PROOFSTEP]
rw [rpow_neg hy'.le, rpow_neg hxR.le, inv_le_inv (rpow_pos_of_pos hy' _) (rpow_pos_of_pos hxR _)]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
hxR : 0 < x + R
hy' : 0 < y
⊢ (x + R) ^ b ≤ y ^ b
[PROOFSTEP]
exact rpow_le_rpow hxR.le hy hb.le
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
hxR : 0 < x + R
hy' : 0 < y
this : y ^ (-b) ≤ (x + R) ^ (-b)
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
[PROOFSTEP]
refine' this.trans _
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
hxR : 0 < x + R
hy' : 0 < y
this : y ^ (-b) ≤ (x + R) ^ (-b)
⊢ (x + R) ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
[PROOFSTEP]
rw [← mul_rpow one_half_pos.le hx.1.le, rpow_neg (mul_pos one_half_pos hx.1).le, rpow_neg hxR.le]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
hxR : 0 < x + R
hy' : 0 < y
this : y ^ (-b) ≤ (x + R) ^ (-b)
⊢ ((x + R) ^ b)⁻¹ ≤ ((1 / 2 * x) ^ b)⁻¹
[PROOFSTEP]
refine' inv_le_inv_of_le (rpow_pos_of_pos (mul_pos one_half_pos hx.1) _) _
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
hxR : 0 < x + R
hy' : 0 < y
this : y ^ (-b) ≤ (x + R) ^ (-b)
⊢ (1 / 2 * x) ^ b ≤ (x + R) ^ b
[PROOFSTEP]
exact rpow_le_rpow (mul_pos one_half_pos hx.1).le (by linarith) hb.le
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
hxR : 0 < x + R
hy' : 0 < y
this : y ^ (-b) ≤ (x + R) ^ (-b)
⊢ 1 / 2 * x ≤ x + R
[PROOFSTEP]
linarith
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
⊢ (fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atTop] fun x => |x| ^ (-b)
[PROOFSTEP]
obtain ⟨c, hc, hc'⟩ := hf.exists_pos
[GOAL]
case intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
hc' : IsBigOWith c atTop ↑f fun x => |x| ^ (-b)
⊢ (fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atTop] fun x => |x| ^ (-b)
[PROOFSTEP]
simp only [IsBigO, IsBigOWith, eventually_atTop] at hc' ⊢
[GOAL]
case intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
hc' : ∃ a, ∀ (b_1 : ℝ), b_1 ≥ a → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
⊢ ∃ c a, ∀ (b_1 : ℝ), b_1 ≥ a → ‖‖ContinuousMap.restrict (Icc (b_1 + R) (b_1 + S)) f‖‖ ≤ c * ‖|b_1| ^ (-b)‖
[PROOFSTEP]
obtain ⟨d, hd⟩ := hc'
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
⊢ ∃ c a, ∀ (b_1 : ℝ), b_1 ≥ a → ‖‖ContinuousMap.restrict (Icc (b_1 + R) (b_1 + S)) f‖‖ ≤ c * ‖|b_1| ^ (-b)‖
[PROOFSTEP]
refine' ⟨c * (1 / 2) ^ (-b), ⟨max (1 + max 0 (-2 * R)) (d - R), fun x hx => _⟩⟩
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : x ≥ max (1 + max 0 (-2 * R)) (d - R)
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
[PROOFSTEP]
rw [ge_iff_le, max_le_iff] at hx 
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
[PROOFSTEP]
have hx' : max 0 (-2 * R) < x := by linarith
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
⊢ max 0 (-2 * R) < x
[PROOFSTEP]
linarith
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : max 0 (-2 * R) < x
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
[PROOFSTEP]
rw [max_lt_iff] at hx' 
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
[PROOFSTEP]
rw [norm_norm,
  ContinuousMap.norm_le _ (mul_nonneg (mul_nonneg hc.le <| rpow_nonneg_of_nonneg one_half_pos.le _) (norm_nonneg _))]
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
⊢ ∀ (x_1 : ↑(Icc (x + R) (x + S))),
    ‖↑(ContinuousMap.restrict (Icc (x + R) (x + S)) f) x_1‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
[PROOFSTEP]
refine' fun y => (hd y.1 (by linarith [hx.1, y.2.1])).trans _
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
⊢ ↑y ≥ d
[PROOFSTEP]
linarith [hx.1, y.2.1]
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
⊢ c * ‖|↑y| ^ (-b)‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
[PROOFSTEP]
have A : ∀ x : ℝ, 0 ≤ |x| ^ (-b) := fun x => by positivity
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x✝ : ℝ
hx : 1 + max 0 (-2 * R) ≤ x✝ ∧ d - R ≤ x✝
hx' : 0 < x✝ ∧ -2 * R < x✝
y : ↑(Icc (x✝ + R) (x✝ + S))
x : ℝ
⊢ 0 ≤ |x| ^ (-b)
[PROOFSTEP]
positivity
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ c * ‖|↑y| ^ (-b)‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
[PROOFSTEP]
rw [mul_assoc, mul_le_mul_left hc, norm_of_nonneg (A _), norm_of_nonneg (A _)]
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ |↑y| ^ (-b) ≤ (1 / 2) ^ (-b) * |x| ^ (-b)
[PROOFSTEP]
convert claim x (by linarith only [hx.1]) y.1 y.2.1
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ max 0 (-2 * R) < x
[PROOFSTEP]
linarith only [hx.1]
[GOAL]
case h.e'_3.h.e'_5
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ |↑y| = ↑y
[PROOFSTEP]
apply abs_of_nonneg
[GOAL]
case h.e'_3.h.e'_5.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ 0 ≤ ↑y
[PROOFSTEP]
linarith [y.2.1]
[GOAL]
case h.e'_4.h.e'_6.h.e'_5
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : 0 < c
d : ℝ
hd : ∀ (b_1 : ℝ), b_1 ≥ d → ‖↑f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ |x| = x
[PROOFSTEP]
exact abs_of_pos hx'.1
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
⊢ (fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atBot] fun x => |x| ^ (-b)
[PROOFSTEP]
have h1 : IsBigO atTop (f.comp (ContinuousMap.mk _ continuous_neg)) fun x : ℝ => |x| ^ (-b) :=
  by
  convert hf.comp_tendsto tendsto_neg_atTop_atBot using 1
  ext1 x; simp only [Function.comp_apply, abs_neg]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
⊢ ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
[PROOFSTEP]
convert hf.comp_tendsto tendsto_neg_atTop_atBot using 1
[GOAL]
case h.e'_8
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
⊢ (fun x => |x| ^ (-b)) = (fun x => |x| ^ (-b)) ∘ Neg.neg
[PROOFSTEP]
ext1 x
[GOAL]
case h.e'_8.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S x : ℝ
⊢ |x| ^ (-b) = ((fun x => |x| ^ (-b)) ∘ Neg.neg) x
[PROOFSTEP]
simp only [Function.comp_apply, abs_neg]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
⊢ (fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atBot] fun x => |x| ^ (-b)
[PROOFSTEP]
have h2 := (isBigO_norm_Icc_restrict_atTop hb h1 (-S) (-R)).comp_tendsto tendsto_neg_atBot_atTop
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    ((fun x => |x| ^ (-b)) ∘ Neg.neg)
⊢ (fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atBot] fun x => |x| ^ (-b)
[PROOFSTEP]
have : (fun x : ℝ => |x| ^ (-b)) ∘ Neg.neg = fun x : ℝ => |x| ^ (-b) := by ext1 x;
  simp only [Function.comp_apply, abs_neg]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    ((fun x => |x| ^ (-b)) ∘ Neg.neg)
⊢ (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
[PROOFSTEP]
ext1 x
[GOAL]
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    ((fun x => |x| ^ (-b)) ∘ Neg.neg)
x : ℝ
⊢ ((fun x => |x| ^ (-b)) ∘ Neg.neg) x = |x| ^ (-b)
[PROOFSTEP]
simp only [Function.comp_apply, abs_neg]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    ((fun x => |x| ^ (-b)) ∘ Neg.neg)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
⊢ (fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atBot] fun x => |x| ^ (-b)
[PROOFSTEP]
rw [this] at h2 
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
⊢ (fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atBot] fun x => |x| ^ (-b)
[PROOFSTEP]
refine' (isBigO_of_le _ fun x => _).trans h2
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x : ℝ
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤
    ‖((fun x =>
            ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
          Neg.neg)
        x‖
[PROOFSTEP]
rw [norm_norm, Function.comp_apply, norm_norm, ContinuousMap.norm_le _ (norm_nonneg _)]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x : ℝ
⊢ ∀ (x_1 : ↑(Icc (x + R) (x + S))),
    ‖↑(ContinuousMap.restrict (Icc (x + R) (x + S)) f) x_1‖ ≤
      ‖ContinuousMap.restrict (Icc (-x + -S) (-x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case mk
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ ‖↑(ContinuousMap.restrict (Icc (x✝ + R) (x✝ + S)) f) { val := x, property := hx }‖ ≤
    ‖ContinuousMap.restrict (Icc (-x✝ + -S) (-x✝ + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖
[PROOFSTEP]
rw [ContinuousMap.restrict_apply_mk]
[GOAL]
case mk
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ ‖↑f x‖ ≤ ‖ContinuousMap.restrict (Icc (-x✝ + -S) (-x✝ + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖
[PROOFSTEP]
refine' (le_of_eq _).trans (ContinuousMap.norm_coe_le_norm _ ⟨-x, _⟩)
[GOAL]
case mk.refine'_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ ‖↑f x‖ =
    ‖↑(ContinuousMap.restrict (Icc (-x✝ + -S) (-x✝ + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a)))
        { val := -x, property := ?mk.refine'_2 }‖
case mk.refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ∈ Icc (-x✝ + -S) (-x✝ + -R)
[PROOFSTEP]
rw [ContinuousMap.restrict_apply_mk, ContinuousMap.comp_apply, ContinuousMap.coe_mk, ContinuousMap.coe_mk, neg_neg]
[GOAL]
case mk.refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ∈ Icc (-x✝ + -S) (-x✝ + -R)
case mk.refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ∈ Icc (-x✝ + -S) (-x✝ + -R)
case mk.refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ∈ Icc (-x✝ + -S) (-x✝ + -R)
case mk.refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ∈ Icc (-x✝ + -S) (-x✝ + -R)
case mk.refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ∈ Icc (-x✝ + -S) (-x✝ + -R)
case mk.refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ∈ Icc (-x✝ + -S) (-x✝ + -R)
[PROOFSTEP]
exact ⟨by linarith [hx.2], by linarith [hx.1]⟩
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x✝ + -S ≤ -x
[PROOFSTEP]
linarith [hx.2]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ↑(ContinuousMap.comp f (ContinuousMap.mk fun a => -a)) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x => ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (ContinuousMap.comp f (ContinuousMap.mk fun a => -a))‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ≤ -x✝ + -R
[PROOFSTEP]
linarith [hx.1]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
⊢ (fun x => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖) =O[cocompact ℝ] fun x =>
    |x| ^ (-b)
[PROOFSTEP]
obtain ⟨r, hr⟩ := K.isCompact.bounded.subset_ball 0
[GOAL]
case intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Metric.closedBall 0 r
⊢ (fun x => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖) =O[cocompact ℝ] fun x =>
    |x| ^ (-b)
[PROOFSTEP]
rw [closedBall_eq_Icc, zero_add, zero_sub] at hr 
[GOAL]
case intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
⊢ (fun x => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖) =O[cocompact ℝ] fun x =>
    |x| ^ (-b)
[PROOFSTEP]
have : ∀ x : ℝ, ‖(f.comp (ContinuousMap.addRight x)).restrict K‖ ≤ ‖f.restrict (Icc (x - r) (x + r))‖ :=
  by
  intro x
  rw [ContinuousMap.norm_le _ (norm_nonneg _)]
  rintro ⟨y, hy⟩
  refine' (le_of_eq _).trans (ContinuousMap.norm_coe_le_norm _ ⟨y + x, _⟩)
  · simp_rw [ContinuousMap.restrict_apply, ContinuousMap.comp_apply, ContinuousMap.coe_addRight]
  · exact ⟨by linarith [(hr hy).1], by linarith [(hr hy).2]⟩
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
⊢ ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
[PROOFSTEP]
intro x
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x : ℝ
⊢ ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
    ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
[PROOFSTEP]
rw [ContinuousMap.norm_le _ (norm_nonneg _)]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x : ℝ
⊢ ∀ (x_1 : ↑↑K),
    ‖↑(ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))) x_1‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case mk
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ ↑K
⊢ ‖↑(ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))) { val := y, property := hy }‖ ≤
    ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
[PROOFSTEP]
refine' (le_of_eq _).trans (ContinuousMap.norm_coe_le_norm _ ⟨y + x, _⟩)
[GOAL]
case mk.refine'_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ ↑K
⊢ ‖↑(ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))) { val := y, property := hy }‖ =
    ‖↑(ContinuousMap.restrict (Icc (x - r) (x + r)) f) { val := y + x, property := ?mk.refine'_2 }‖
[PROOFSTEP]
simp_rw [ContinuousMap.restrict_apply, ContinuousMap.comp_apply, ContinuousMap.coe_addRight]
[GOAL]
case mk.refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ ↑K
⊢ y + x ∈ Icc (x - r) (x + r)
[PROOFSTEP]
exact ⟨by linarith [(hr hy).1], by linarith [(hr hy).2]⟩
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ ↑K
⊢ x - r ≤ y + x
[PROOFSTEP]
linarith [(hr hy).1]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ ↑K
⊢ y + x ≤ x + r
[PROOFSTEP]
linarith [(hr hy).2]
[GOAL]
case intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ↑f =O[cocompact ℝ] fun x => |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
⊢ (fun x => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖) =O[cocompact ℝ] fun x =>
    |x| ^ (-b)
[PROOFSTEP]
simp_rw [cocompact_eq, isBigO_sup] at hf ⊢
[GOAL]
case intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (↑f =O[atBot] fun x => |x| ^ (-b)) ∧ ↑f =O[atTop] fun x => |x| ^ (-b)
⊢ ((fun x => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖) =O[atBot] fun x =>
      |x| ^ (-b)) ∧
    (fun x => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖) =O[atTop] fun x =>
      |x| ^ (-b)
[PROOFSTEP]
constructor
[GOAL]
case intro.left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (↑f =O[atBot] fun x => |x| ^ (-b)) ∧ ↑f =O[atTop] fun x => |x| ^ (-b)
⊢ (fun x => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖) =O[atBot] fun x =>
    |x| ^ (-b)
[PROOFSTEP]
refine' (isBigO_of_le atBot _).trans (isBigO_norm_Icc_restrict_atBot hb hf.1 (-r) r)
[GOAL]
case intro.left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (↑f =O[atBot] fun x => |x| ^ (-b)) ∧ ↑f =O[atTop] fun x => |x| ^ (-b)
⊢ ∀ (x : ℝ),
    ‖‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖‖ ≤
      ‖‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖‖
[PROOFSTEP]
simp_rw [norm_norm]
[GOAL]
case intro.left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (↑f =O[atBot] fun x => |x| ^ (-b)) ∧ ↑f =O[atTop] fun x => |x| ^ (-b)
⊢ ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖
[PROOFSTEP]
exact this
[GOAL]
case intro.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (↑f =O[atBot] fun x => |x| ^ (-b)) ∧ ↑f =O[atTop] fun x => |x| ^ (-b)
⊢ (fun x => ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖) =O[atTop] fun x =>
    |x| ^ (-b)
[PROOFSTEP]
refine' (isBigO_of_le atTop _).trans (isBigO_norm_Icc_restrict_atTop hb hf.2 (-r) r)
[GOAL]
case intro.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (↑f =O[atBot] fun x => |x| ^ (-b)) ∧ ↑f =O[atTop] fun x => |x| ^ (-b)
⊢ ∀ (x : ℝ),
    ‖‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖‖ ≤
      ‖‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖‖
[PROOFSTEP]
simp_rw [norm_norm]
[GOAL]
case intro.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (↑f =O[atBot] fun x => |x| ^ (-b)) ∧ ↑f =O[atTop] fun x => |x| ^ (-b)
⊢ ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (ContinuousMap.comp f (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖
[PROOFSTEP]
exact this
[GOAL]
f g : SchwartzMap ℝ ℂ
hfg : 𝓕 ↑f = ↑g
⊢ ∑' (n : ℤ), ↑f ↑n = ∑' (n : ℤ), ↑g ↑n
[PROOFSTEP]
simp_rw [← hfg]
[GOAL]
f g : SchwartzMap ℝ ℂ
hfg : 𝓕 ↑f = ↑g
⊢ ∑' (n : ℤ), ↑f ↑n = ∑' (n : ℤ), 𝓕 ↑f ↑n
[PROOFSTEP]
rw [Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay f.continuous one_lt_two (f.isBigO_cocompact_rpow (-2))]
[GOAL]
f g : SchwartzMap ℝ ℂ
hfg : 𝓕 ↑f = ↑g
⊢ 𝓕 ↑f =O[cocompact ℝ] fun x => |x| ^ (-2)
[PROOFSTEP]
rw [hfg]
[GOAL]
f g : SchwartzMap ℝ ℂ
hfg : 𝓕 ↑f = ↑g
⊢ ↑g =O[cocompact ℝ] fun x => |x| ^ (-2)
[PROOFSTEP]
exact g.isBigO_cocompact_rpow (-2)
