HardyZeta.FiniteDifference

            
              11.3. HardyZeta.FiniteDifference🔗
            def modifiedDifference (h : ℝ) (f : ℝ → ℝ) (x : ℝ) : ℝ :=
  f (x + h) + f (x - h) - 2 * Real.cos (h / 2) * f x

/-- The multiplier on the hyperbolic cosine kernel. -/def differenceMultiplier (h t : ℝ) : ℝ :=
  2 * (Real.cosh (h * t) - Real.cos (h / 2))theorem modifiedDifference_cos (h x : ℝ) :
    modifiedDifference h (fun x ↦ Real.cos (x / 2)) x = 0 := byh:ℝx:ℝ⊢ modifiedDifference h (fun x => Real.cos (x / 2)) x = 0
  simp only [modifiedDifference, add_div, sub_div, Real.cos_add, Real.cos_sub]h:ℝx:ℝ⊢ Real.cos (x / 2) * Real.cos (h / 2) - Real.sin (x / 2) * Real.sin (h / 2) +
      (Real.cos (x / 2) * Real.cos (h / 2) + Real.sin (x / 2) * Real.sin (h / 2)) -
    2 * Real.cos (h / 2) * Real.cos (x / 2) =
  0
  ringAll goals completed! 🐙theorem modifiedDifference_cosh (h t x : ℝ) :
    modifiedDifference h (fun x ↦ Real.cosh (x * t)) x =
      differenceMultiplier h t * Real.cosh (x * t) := byh:ℝt:ℝx:ℝ⊢ modifiedDifference h (fun x => Real.cosh (x * t)) x = differenceMultiplier h t * Real.cosh (x * t)
  simp only [modifiedDifference, differenceMultiplier, add_mul, sub_mul,
    Real.cosh_add, Real.cosh_sub]h:ℝt:ℝx:ℝ⊢ Real.cosh (x * t) * Real.cosh (h * t) + Real.sinh (x * t) * Real.sinh (h * t) +
      (Real.cosh (x * t) * Real.cosh (h * t) - Real.sinh (x * t) * Real.sinh (h * t)) -
    2 * Real.cos (h / 2) * Real.cosh (x * t) =
  2 * (Real.cosh (h * t) - Real.cos (h / 2)) * Real.cosh (x * t)
  ringAll goals completed! 🐙theorem differenceMultiplier_nonneg (h t : ℝ) :
    0 ≤ differenceMultiplier h t := byh:ℝt:ℝ⊢ 0 ≤ differenceMultiplier h t
  have := Real.one_le_cosh (h * t)h:ℝt:ℝthis:1 ≤ Real.cosh (h * t)⊢ 0 ≤ differenceMultiplier h t
  have := Real.cos_le_one (h / 2)h:ℝt:ℝthis✝:1 ≤ Real.cosh (h * t)this:Real.cos (h / 2) ≤ 1⊢ 0 ≤ differenceMultiplier h t
  unfold differenceMultiplierh:ℝt:ℝthis✝:1 ≤ Real.cosh (h * t)this:Real.cos (h / 2) ≤ 1⊢ 0 ≤ 2 * (Real.cosh (h * t) - Real.cos (h / 2))
  linarithAll goals completed! 🐙theorem modifiedDifference_const_mul (h c : ℝ) (f : ℝ → ℝ) :
    modifiedDifference h (fun x ↦ c * f x) =
      fun x ↦ c * modifiedDifference h f x := byh:ℝc:ℝf:ℝ → ℝ⊢ (modifiedDifference h fun x => c * f x) = fun x => c * modifiedDifference h f x
  funext xh:ℝc:ℝf:ℝ → ℝx:ℝ⊢ modifiedDifference h (fun x => c * f x) x = c * modifiedDifference h f x
  simp only [modifiedDifference]h:ℝc:ℝf:ℝ → ℝx:ℝ⊢ c * f (x + h) + c * f (x - h) - 2 * Real.cos (h / 2) * (c * f x) =
  c * (f (x + h) + f (x - h) - 2 * Real.cos (h / 2) * f x)
  ringAll goals completed! 🐙theorem iterate_modifiedDifference_cosh (h t : ℝ) (k : ℕ) :
    (modifiedDifference h)^[k] (fun x ↦ Real.cosh (x * t)) =
      fun x ↦ differenceMultiplier h t ^ k * Real.cosh (x * t) := byh:ℝt:ℝk:ℕ⊢ ((modifiedDifference h)^[k] fun x => Real.cosh (x * t)) = fun x => differenceMultiplier h t ^ k * Real.cosh (x * t)
  induction k with
  | zero =>zeroh:ℝt:ℝ⊢ ((modifiedDifference h)^[0] fun x => Real.cosh (x * t)) = fun x => differenceMultiplier h t ^ 0 * Real.cosh (x * t) simpAll goals completed! 🐙
  | succ k ih =>succh:ℝt:ℝk:ℕih:((modifiedDifference h)^[k] fun x => Real.cosh (x * t)) = fun x => differenceMultiplier h t ^ k * Real.cosh (x * t)⊢ ((modifiedDifference h)^[k + 1] fun x => Real.cosh (x * t)) = fun x =>
  differenceMultiplier h t ^ (k + 1) * Real.cosh (x * t)
    rw [Function.iterate_succ_apply',succh:ℝt:ℝk:ℕih:((modifiedDifference h)^[k] fun x => Real.cosh (x * t)) = fun x => differenceMultiplier h t ^ k * Real.cosh (x * t)⊢ modifiedDifference h ((modifiedDifference h)^[k] fun x => Real.cosh (x * t)) = fun x =>
  differenceMultiplier h t ^ (k + 1) * Real.cosh (x * t) ih,succh:ℝt:ℝk:ℕih:((modifiedDifference h)^[k] fun x => Real.cosh (x * t)) = fun x => differenceMultiplier h t ^ k * Real.cosh (x * t)⊢ (modifiedDifference h fun x => differenceMultiplier h t ^ k * Real.cosh (x * t)) = fun x =>
  differenceMultiplier h t ^ (k + 1) * Real.cosh (x * t) modifiedDifference_const_mulsucch:ℝt:ℝk:ℕih:((modifiedDifference h)^[k] fun x => Real.cosh (x * t)) = fun x => differenceMultiplier h t ^ k * Real.cosh (x * t)⊢ (fun x => differenceMultiplier h t ^ k * modifiedDifference h (fun x => Real.cosh (x * t)) x) = fun x =>
  differenceMultiplier h t ^ (k + 1) * Real.cosh (x * t)]succh:ℝt:ℝk:ℕih:((modifiedDifference h)^[k] fun x => Real.cosh (x * t)) = fun x => differenceMultiplier h t ^ k * Real.cosh (x * t)⊢ (fun x => differenceMultiplier h t ^ k * modifiedDifference h (fun x => Real.cosh (x * t)) x) = fun x =>
  differenceMultiplier h t ^ (k + 1) * Real.cosh (x * t)
    funext xsucch:ℝt:ℝk:ℕih:((modifiedDifference h)^[k] fun x => Real.cosh (x * t)) = fun x => differenceMultiplier h t ^ k * Real.cosh (x * t)x:ℝ⊢ differenceMultiplier h t ^ k * modifiedDifference h (fun x => Real.cosh (x * t)) x =
  differenceMultiplier h t ^ (k + 1) * Real.cosh (x * t)
    rw [modifiedDifference_cosh,succh:ℝt:ℝk:ℕih:((modifiedDifference h)^[k] fun x => Real.cosh (x * t)) = fun x => differenceMultiplier h t ^ k * Real.cosh (x * t)x:ℝ⊢ differenceMultiplier h t ^ k * (differenceMultiplier h t * Real.cosh (x * t)) =
  differenceMultiplier h t ^ (k + 1) * Real.cosh (x * t) pow_succsucch:ℝt:ℝk:ℕih:((modifiedDifference h)^[k] fun x => Real.cosh (x * t)) = fun x => differenceMultiplier h t ^ k * Real.cosh (x * t)x:ℝ⊢ differenceMultiplier h t ^ k * (differenceMultiplier h t * Real.cosh (x * t)) =
  differenceMultiplier h t ^ k * differenceMultiplier h t * Real.cosh (x * t)]succh:ℝt:ℝk:ℕih:((modifiedDifference h)^[k] fun x => Real.cosh (x * t)) = fun x => differenceMultiplier h t ^ k * Real.cosh (x * t)x:ℝ⊢ differenceMultiplier h t ^ k * (differenceMultiplier h t * Real.cosh (x * t)) =
  differenceMultiplier h t ^ k * differenceMultiplier h t * Real.cosh (x * t)
    ringAll goals completed! 🐙theorem differenceMultiplier_eq_squares (h t : ℝ) :
    differenceMultiplier h t =
      4 * (Real.sinh (h * t / 2) ^ 2 + Real.sin (h / 4) ^ 2) := byh:ℝt:ℝ⊢ differenceMultiplier h t = 4 * (Real.sinh (h * t / 2) ^ 2 + Real.sin (h / 4) ^ 2)
  have hh : h * t = h * t / 2 + h * t / 2 := by ringh:ℝt:ℝhh:h * t = h * t / 2 + h * t / 2⊢ differenceMultiplier h t = 4 * (Real.sinh (h * t / 2) ^ 2 + Real.sin (h / 4) ^ 2)
  have hc : h / 2 = h / 4 + h / 4 := by ringh:ℝt:ℝhh:h * t = h * t / 2 + h * t / 2hc:h / 2 = h / 4 + h / 4⊢ differenceMultiplier h t = 4 * (Real.sinh (h * t / 2) ^ 2 + Real.sin (h / 4) ^ 2)
  unfold differenceMultiplierh:ℝt:ℝhh:h * t = h * t / 2 + h * t / 2hc:h / 2 = h / 4 + h / 4⊢ 2 * (Real.cosh (h * t) - Real.cos (h / 2)) = 4 * (Real.sinh (h * t / 2) ^ 2 + Real.sin (h / 4) ^ 2)
  conv_lhs => rw [hh, hc, Real.cosh_add, Real.cos_add]h:ℝt:ℝhh:h * t = h * t / 2 + h * t / 2hc:h / 2 = h / 4 + h / 4| 2 *
  (Real.cosh (h * t / 2) * Real.cosh (h * t / 2) + Real.sinh (h * t / 2) * Real.sinh (h * t / 2) -
    (Real.cos (h / 4) * Real.cos (h / 4) - Real.sin (h / 4) * Real.sin (h / 4)))
  have hs := Real.cosh_sq_sub_sinh_sq (h * t / 2)h:ℝt:ℝhh:h * t = h * t / 2 + h * t / 2hc:h / 2 = h / 4 + h / 4hs:Real.cosh (h * t / 2) ^ 2 - Real.sinh (h * t / 2) ^ 2 = 1⊢ 2 *
    (Real.cosh (h * t / 2) * Real.cosh (h * t / 2) + Real.sinh (h * t / 2) * Real.sinh (h * t / 2) -
      (Real.cos (h / 4) * Real.cos (h / 4) - Real.sin (h / 4) * Real.sin (h / 4))) =
  4 * (Real.sinh (h * t / 2) ^ 2 + Real.sin (h / 4) ^ 2)
  have ht := Real.sin_sq_add_cos_sq (h / 4)h:ℝt:ℝhh:h * t = h * t / 2 + h * t / 2hc:h / 2 = h / 4 + h / 4hs:Real.cosh (h * t / 2) ^ 2 - Real.sinh (h * t / 2) ^ 2 = 1ht:Real.sin (h / 4) ^ 2 + Real.cos (h / 4) ^ 2 = 1⊢ 2 *
    (Real.cosh (h * t / 2) * Real.cosh (h * t / 2) + Real.sinh (h * t / 2) * Real.sinh (h * t / 2) -
      (Real.cos (h / 4) * Real.cos (h / 4) - Real.sin (h / 4) * Real.sin (h / 4))) =
  4 * (Real.sinh (h * t / 2) ^ 2 + Real.sin (h / 4) ^ 2)
  nlinarithAll goals completed! 🐙theorem tendsto_differenceMultiplier_div_sq (t : ℝ) :
    Tendsto (fun h : ℝ ↦ differenceMultiplier h t / h ^ 2)
      (𝓝[>] 0) (𝓝 (t ^ 2 + 1 / 4)) := byt:ℝ⊢ Tendsto (fun h => differenceMultiplier h t / h ^ 2) (𝓝[>] 0) (𝓝 (t ^ 2 + 1 / 4))
  have hs : HasDerivAt (fun h : ℝ ↦ Real.sinh (h * t / 2)) (t / 2) 0 := by
    convert (((hasDerivAt_id (0 : ℝ)).mul_const t).div_const 2).sinh using 1e'_8t:ℝ⊢ (fun h => Real.sinh (h * t / 2)) = fun x => Real.sinh (id x * t / 2)e'_9t:ℝ⊢ t / 2 = Real.cosh (id 0 * t / 2) * (1 * t / 2) <;>e'_8t:ℝ⊢ (fun h => Real.sinh (h * t / 2)) = fun x => Real.sinh (id x * t / 2)e'_9t:ℝ⊢ t / 2 = Real.cosh (id 0 * t / 2) * (1 * t / 2) simpt:ℝhs:HasDerivAt (fun h => Real.sinh (h * t / 2)) (t / 2) 0⊢ Tendsto (fun h => differenceMultiplier h t / h ^ 2) (𝓝[>] 0) (𝓝 (t ^ 2 + 1 / 4))
  have hc : HasDerivAt (fun h : ℝ ↦ Real.sin (h / 4)) (1 / 4) 0 := by
    convert ((hasDerivAt_id (0 : ℝ)).div_const 4).sin using 1e'_8t:ℝhs:HasDerivAt (fun h => Real.sinh (h * t / 2)) (t / 2) 0⊢ (fun h => Real.sin (h / 4)) = fun x => Real.sin (id x / 4)e'_9t:ℝhs:HasDerivAt (fun h => Real.sinh (h * t / 2)) (t / 2) 0⊢ 1 / 4 = Real.cos (id 0 / 4) * (1 / 4) <;>e'_8t:ℝhs:HasDerivAt (fun h => Real.sinh (h * t / 2)) (t / 2) 0⊢ (fun h => Real.sin (h / 4)) = fun x => Real.sin (id x / 4)e'_9t:ℝhs:HasDerivAt (fun h => Real.sinh (h * t / 2)) (t / 2) 0⊢ 1 / 4 = Real.cos (id 0 / 4) * (1 / 4) simpt:ℝhs:HasDerivAt (fun h => Real.sinh (h * t / 2)) (t / 2) 0hc:HasDerivAt (fun h => Real.sin (h / 4)) (1 / 4) 0⊢ Tendsto (fun h => differenceMultiplier h t / h ^ 2) (𝓝[>] 0) (𝓝 (t ^ 2 + 1 / 4))
  have hsl : Tendsto (fun h : ℝ ↦ Real.sinh (h * t / 2) / h)
      (𝓝[>] 0) (𝓝 (t / 2)) := by
    simpa [smul_eq_mul, div_eq_mul_inv, mul_comm] using hs.tendsto_slope_zero_rightt:ℝhs:HasDerivAt (fun h => Real.sinh (h * t / 2)) (t / 2) 0hc:HasDerivAt (fun h => Real.sin (h / 4)) (1 / 4) 0hsl:Tendsto (fun h => Real.sinh (h * t / 2) / h) (𝓝[>] 0) (𝓝 (t / 2))⊢ Tendsto (fun h => differenceMultiplier h t / h ^ 2) (𝓝[>] 0) (𝓝 (t ^ 2 + 1 / 4))
  have hcl : Tendsto (fun h : ℝ ↦ Real.sin (h / 4) / h)
      (𝓝[>] 0) (𝓝 (1 / 4)) := by
    simpa [smul_eq_mul, div_eq_mul_inv, mul_comm] using hc.tendsto_slope_zero_rightt:ℝhs:HasDerivAt (fun h => Real.sinh (h * t / 2)) (t / 2) 0hc:HasDerivAt (fun h => Real.sin (h / 4)) (1 / 4) 0hsl:Tendsto (fun h => Real.sinh (h * t / 2) / h) (𝓝[>] 0) (𝓝 (t / 2))hcl:Tendsto (fun h => Real.sin (h / 4) / h) (𝓝[>] 0) (𝓝 (1 / 4))⊢ Tendsto (fun h => differenceMultiplier h t / h ^ 2) (𝓝[>] 0) (𝓝 (t ^ 2 + 1 / 4))
  have hl := ((hsl.pow 2).add (hcl.pow 2)).const_mul 4t:ℝhs:HasDerivAt (fun h => Real.sinh (h * t / 2)) (t / 2) 0hc:HasDerivAt (fun h => Real.sin (h / 4)) (1 / 4) 0hsl:Tendsto (fun h => Real.sinh (h * t / 2) / h) (𝓝[>] 0) (𝓝 (t / 2))hcl:Tendsto (fun h => Real.sin (h / 4) / h) (𝓝[>] 0) (𝓝 (1 / 4))hl:Tendsto (fun x => 4 * ((Real.sinh (x * t / 2) / x) ^ 2 + (Real.sin (x / 4) / x) ^ 2)) (𝓝[>] 0)
  (𝓝 (4 * ((t / 2) ^ 2 + (1 / 4) ^ 2)))⊢ Tendsto (fun h => differenceMultiplier h t / h ^ 2) (𝓝[>] 0) (𝓝 (t ^ 2 + 1 / 4))
  convert hl using 1e'_3t:ℝhs:HasDerivAt (fun h => Real.sinh (h * t / 2)) (t / 2) 0hc:HasDerivAt (fun h => Real.sin (h / 4)) (1 / 4) 0hsl:Tendsto (fun h => Real.sinh (h * t / 2) / h) (𝓝[>] 0) (𝓝 (t / 2))hcl:Tendsto (fun h => Real.sin (h / 4) / h) (𝓝[>] 0) (𝓝 (1 / 4))hl:Tendsto (fun x => 4 * ((Real.sinh (x * t / 2) / x) ^ 2 + (Real.sin (x / 4) / x) ^ 2)) (𝓝[>] 0)
  (𝓝 (4 * ((t / 2) ^ 2 + (1 / 4) ^ 2)))⊢ (fun h => differenceMultiplier h t / h ^ 2) = fun x =>
  4 * ((Real.sinh (x * t / 2) / x) ^ 2 + (Real.sin (x / 4) / x) ^ 2)e'_5t:ℝhs:HasDerivAt (fun h => Real.sinh (h * t / 2)) (t / 2) 0hc:HasDerivAt (fun h => Real.sin (h / 4)) (1 / 4) 0hsl:Tendsto (fun h => Real.sinh (h * t / 2) / h) (𝓝[>] 0) (𝓝 (t / 2))hcl:Tendsto (fun h => Real.sin (h / 4) / h) (𝓝[>] 0) (𝓝 (1 / 4))hl:Tendsto (fun x => 4 * ((Real.sinh (x * t / 2) / x) ^ 2 + (Real.sin (x / 4) / x) ^ 2)) (𝓝[>] 0)
  (𝓝 (4 * ((t / 2) ^ 2 + (1 / 4) ^ 2)))⊢ 𝓝 (t ^ 2 + 1 / 4) = 𝓝 (4 * ((t / 2) ^ 2 + (1 / 4) ^ 2))
  ·e'_3t:ℝhs:HasDerivAt (fun h => Real.sinh (h * t / 2)) (t / 2) 0hc:HasDerivAt (fun h => Real.sin (h / 4)) (1 / 4) 0hsl:Tendsto (fun h => Real.sinh (h * t / 2) / h) (𝓝[>] 0) (𝓝 (t / 2))hcl:Tendsto (fun h => Real.sin (h / 4) / h) (𝓝[>] 0) (𝓝 (1 / 4))hl:Tendsto (fun x => 4 * ((Real.sinh (x * t / 2) / x) ^ 2 + (Real.sin (x / 4) / x) ^ 2)) (𝓝[>] 0)
  (𝓝 (4 * ((t / 2) ^ 2 + (1 / 4) ^ 2)))⊢ (fun h => differenceMultiplier h t / h ^ 2) = fun x =>
  4 * ((Real.sinh (x * t / 2) / x) ^ 2 + (Real.sin (x / 4) / x) ^ 2) funext he'_3t:ℝhs:HasDerivAt (fun h => Real.sinh (h * t / 2)) (t / 2) 0hc:HasDerivAt (fun h => Real.sin (h / 4)) (1 / 4) 0hsl:Tendsto (fun h => Real.sinh (h * t / 2) / h) (𝓝[>] 0) (𝓝 (t / 2))hcl:Tendsto (fun h => Real.sin (h / 4) / h) (𝓝[>] 0) (𝓝 (1 / 4))hl:Tendsto (fun x => 4 * ((Real.sinh (x * t / 2) / x) ^ 2 + (Real.sin (x / 4) / x) ^ 2)) (𝓝[>] 0)
  (𝓝 (4 * ((t / 2) ^ 2 + (1 / 4) ^ 2)))h:ℝ⊢ differenceMultiplier h t / h ^ 2 = 4 * ((Real.sinh (h * t / 2) / h) ^ 2 + (Real.sin (h / 4) / h) ^ 2)
    rw [differenceMultiplier_eq_squarese'_3t:ℝhs:HasDerivAt (fun h => Real.sinh (h * t / 2)) (t / 2) 0hc:HasDerivAt (fun h => Real.sin (h / 4)) (1 / 4) 0hsl:Tendsto (fun h => Real.sinh (h * t / 2) / h) (𝓝[>] 0) (𝓝 (t / 2))hcl:Tendsto (fun h => Real.sin (h / 4) / h) (𝓝[>] 0) (𝓝 (1 / 4))hl:Tendsto (fun x => 4 * ((Real.sinh (x * t / 2) / x) ^ 2 + (Real.sin (x / 4) / x) ^ 2)) (𝓝[>] 0)
  (𝓝 (4 * ((t / 2) ^ 2 + (1 / 4) ^ 2)))h:ℝ⊢ 4 * (Real.sinh (h * t / 2) ^ 2 + Real.sin (h / 4) ^ 2) / h ^ 2 =
  4 * ((Real.sinh (h * t / 2) / h) ^ 2 + (Real.sin (h / 4) / h) ^ 2)]e'_3t:ℝhs:HasDerivAt (fun h => Real.sinh (h * t / 2)) (t / 2) 0hc:HasDerivAt (fun h => Real.sin (h / 4)) (1 / 4) 0hsl:Tendsto (fun h => Real.sinh (h * t / 2) / h) (𝓝[>] 0) (𝓝 (t / 2))hcl:Tendsto (fun h => Real.sin (h / 4) / h) (𝓝[>] 0) (𝓝 (1 / 4))hl:Tendsto (fun x => 4 * ((Real.sinh (x * t / 2) / x) ^ 2 + (Real.sin (x / 4) / x) ^ 2)) (𝓝[>] 0)
  (𝓝 (4 * ((t / 2) ^ 2 + (1 / 4) ^ 2)))h:ℝ⊢ 4 * (Real.sinh (h * t / 2) ^ 2 + Real.sin (h / 4) ^ 2) / h ^ 2 =
  4 * ((Real.sinh (h * t / 2) / h) ^ 2 + (Real.sin (h / 4) / h) ^ 2)
    simp only [div_pow]e'_3t:ℝhs:HasDerivAt (fun h => Real.sinh (h * t / 2)) (t / 2) 0hc:HasDerivAt (fun h => Real.sin (h / 4)) (1 / 4) 0hsl:Tendsto (fun h => Real.sinh (h * t / 2) / h) (𝓝[>] 0) (𝓝 (t / 2))hcl:Tendsto (fun h => Real.sin (h / 4) / h) (𝓝[>] 0) (𝓝 (1 / 4))hl:Tendsto (fun x => 4 * ((Real.sinh (x * t / 2) / x) ^ 2 + (Real.sin (x / 4) / x) ^ 2)) (𝓝[>] 0)
  (𝓝 (4 * ((t / 2) ^ 2 + (1 / 4) ^ 2)))h:ℝ⊢ 4 * (Real.sinh (h * t / 2) ^ 2 + Real.sin (h / 4) ^ 2) / h ^ 2 =
  4 * (Real.sinh (h * t / 2) ^ 2 / h ^ 2 + Real.sin (h / 4) ^ 2 / h ^ 2)
    ringAll goals completed! 🐙
  ·e'_5t:ℝhs:HasDerivAt (fun h => Real.sinh (h * t / 2)) (t / 2) 0hc:HasDerivAt (fun h => Real.sin (h / 4)) (1 / 4) 0hsl:Tendsto (fun h => Real.sinh (h * t / 2) / h) (𝓝[>] 0) (𝓝 (t / 2))hcl:Tendsto (fun h => Real.sin (h / 4) / h) (𝓝[>] 0) (𝓝 (1 / 4))hl:Tendsto (fun x => 4 * ((Real.sinh (x * t / 2) / x) ^ 2 + (Real.sin (x / 4) / x) ^ 2)) (𝓝[>] 0)
  (𝓝 (4 * ((t / 2) ^ 2 + (1 / 4) ^ 2)))⊢ 𝓝 (t ^ 2 + 1 / 4) = 𝓝 (4 * ((t / 2) ^ 2 + (1 / 4) ^ 2)) congr 1e'_5t:ℝhs:HasDerivAt (fun h => Real.sinh (h * t / 2)) (t / 2) 0hc:HasDerivAt (fun h => Real.sin (h / 4)) (1 / 4) 0hsl:Tendsto (fun h => Real.sinh (h * t / 2) / h) (𝓝[>] 0) (𝓝 (t / 2))hcl:Tendsto (fun h => Real.sin (h / 4) / h) (𝓝[>] 0) (𝓝 (1 / 4))hl:Tendsto (fun x => 4 * ((Real.sinh (x * t / 2) / x) ^ 2 + (Real.sin (x / 4) / x) ^ 2)) (𝓝[>] 0)
  (𝓝 (4 * ((t / 2) ^ 2 + (1 / 4) ^ 2)))⊢ t ^ 2 + 1 / 4 = 4 * ((t / 2) ^ 2 + (1 / 4) ^ 2)
    ringAll goals completed! 🐙

/-- Moving one difference through an integral requires only the three sampled
functions to be integrable. No endpoint integral is used. -/theorem modifiedDifference_integral {μ : Measure ℝ} (h x : ℝ)
    (f : ℝ → ℝ → ℝ)
    (hp : Integrable (f (x + h)) μ) (hm : Integrable (f (x - h)) μ)
    (hx : Integrable (f x) μ) :
    modifiedDifference h (fun y ↦ ∫ t, f y t ∂μ) x =
      ∫ t, modifiedDifference h (fun y ↦ f y t) x ∂μ := byμ:Measure ℝh:ℝx:ℝf:ℝ → ℝ → ℝhp:Integrable (f (x + h)) μhm:Integrable (f (x - h)) μhx:Integrable (f x) μ⊢ modifiedDifference h (fun y => ∫ (t : ℝ), f y t ∂μ) x = ∫ (t : ℝ), modifiedDifference h (fun y => f y t) x ∂μ
  simp only [modifiedDifference]μ:Measure ℝh:ℝx:ℝf:ℝ → ℝ → ℝhp:Integrable (f (x + h)) μhm:Integrable (f (x - h)) μhx:Integrable (f x) μ⊢ ∫ (t : ℝ), f (x + h) t ∂μ + ∫ (t : ℝ), f (x - h) t ∂μ - 2 * Real.cos (h / 2) * ∫ (t : ℝ), f x t ∂μ =
  ∫ (t : ℝ), f (x + h) t + f (x - h) t - 2 * Real.cos (h / 2) * f x t ∂μ
  have ha : Integrable (fun t ↦ f (x + h) t + f (x - h) t) μ := hp.add hmμ:Measure ℝh:ℝx:ℝf:ℝ → ℝ → ℝhp:Integrable (f (x + h)) μhm:Integrable (f (x - h)) μhx:Integrable (f x) μha:Integrable (fun t => f (x + h) t + f (x - h) t) μ⊢ ∫ (t : ℝ), f (x + h) t ∂μ + ∫ (t : ℝ), f (x - h) t ∂μ - 2 * Real.cos (h / 2) * ∫ (t : ℝ), f x t ∂μ =
  ∫ (t : ℝ), f (x + h) t + f (x - h) t - 2 * Real.cos (h / 2) * f x t ∂μ
  have hb : Integrable (fun t ↦ 2 * Real.cos (h / 2) * f x t) μ :=
    hx.const_mul (2 * Real.cos (h / 2))μ:Measure ℝh:ℝx:ℝf:ℝ → ℝ → ℝhp:Integrable (f (x + h)) μhm:Integrable (f (x - h)) μhx:Integrable (f x) μha:Integrable (fun t => f (x + h) t + f (x - h) t) μhb:Integrable (fun t => 2 * Real.cos (h / 2) * f x t) μ⊢ ∫ (t : ℝ), f (x + h) t ∂μ + ∫ (t : ℝ), f (x - h) t ∂μ - 2 * Real.cos (h / 2) * ∫ (t : ℝ), f x t ∂μ =
  ∫ (t : ℝ), f (x + h) t + f (x - h) t - 2 * Real.cos (h / 2) * f x t ∂μ
  rw [integral_sub ha hb,μ:Measure ℝh:ℝx:ℝf:ℝ → ℝ → ℝhp:Integrable (f (x + h)) μhm:Integrable (f (x - h)) μhx:Integrable (f x) μha:Integrable (fun t => f (x + h) t + f (x - h) t) μhb:Integrable (fun t => 2 * Real.cos (h / 2) * f x t) μ⊢ ∫ (t : ℝ), f (x + h) t ∂μ + ∫ (t : ℝ), f (x - h) t ∂μ - 2 * Real.cos (h / 2) * ∫ (t : ℝ), f x t ∂μ =
  ∫ (a : ℝ), f (x + h) a + f (x - h) a ∂μ - ∫ (a : ℝ), 2 * Real.cos (h / 2) * f x a ∂μ integral_add hp hm,μ:Measure ℝh:ℝx:ℝf:ℝ → ℝ → ℝhp:Integrable (f (x + h)) μhm:Integrable (f (x - h)) μhx:Integrable (f x) μha:Integrable (fun t => f (x + h) t + f (x - h) t) μhb:Integrable (fun t => 2 * Real.cos (h / 2) * f x t) μ⊢ ∫ (t : ℝ), f (x + h) t ∂μ + ∫ (t : ℝ), f (x - h) t ∂μ - 2 * Real.cos (h / 2) * ∫ (t : ℝ), f x t ∂μ =
  ∫ (a : ℝ), f (x + h) a ∂μ + ∫ (a : ℝ), f (x - h) a ∂μ - ∫ (a : ℝ), 2 * Real.cos (h / 2) * f x a ∂μ integral_const_mulμ:Measure ℝh:ℝx:ℝf:ℝ → ℝ → ℝhp:Integrable (f (x + h)) μhm:Integrable (f (x - h)) μhx:Integrable (f x) μha:Integrable (fun t => f (x + h) t + f (x - h) t) μhb:Integrable (fun t => 2 * Real.cos (h / 2) * f x t) μ⊢ ∫ (t : ℝ), f (x + h) t ∂μ + ∫ (t : ℝ), f (x - h) t ∂μ - 2 * Real.cos (h / 2) * ∫ (t : ℝ), f x t ∂μ =
  ∫ (a : ℝ), f (x + h) a ∂μ + ∫ (a : ℝ), f (x - h) a ∂μ - 2 * Real.cos (h / 2) * ∫ (a : ℝ), f x a ∂μ]All goals completed! 🐙

/-- The modified kernel stays integrable using just interior samples. -/theorem integrable_difference_kernel {μ : Measure ℝ} {g : ℝ → ℝ} (h x : ℝ)
    (hp : Integrable (fun t ↦ g t * Real.cosh ((x + h) * t)) μ)
    (hm : Integrable (fun t ↦ g t * Real.cosh ((x - h) * t)) μ)
    (hx : Integrable (fun t ↦ g t * Real.cosh (x * t)) μ) :
    Integrable (fun t ↦ g t * differenceMultiplier h t * Real.cosh (x * t)) μ := byμ:Measure ℝg:ℝ → ℝh:ℝx:ℝhp:Integrable (fun t => g t * Real.cosh ((x + h) * t)) μhm:Integrable (fun t => g t * Real.cosh ((x - h) * t)) μhx:Integrable (fun t => g t * Real.cosh (x * t)) μ⊢ Integrable (fun t => g t * differenceMultiplier h t * Real.cosh (x * t)) μ
  convert (hp.add hm).sub (hx.const_mul (2 * Real.cos (h / 2))) using 1μ:Measure ℝg:ℝ → ℝh:ℝx:ℝhp:Integrable (fun t => g t * Real.cosh ((x + h) * t)) μhm:Integrable (fun t => g t * Real.cosh ((x - h) * t)) μhx:Integrable (fun t => g t * Real.cosh (x * t)) μ⊢ (fun t => g t * differenceMultiplier h t * Real.cosh (x * t)) =
  ((fun t => g t * Real.cosh ((x + h) * t)) + fun t => g t * Real.cosh ((x - h) * t)) - fun x_1 =>
    2 * Real.cos (h / 2) * (g x_1 * Real.cosh (x * x_1))
  funext tμ:Measure ℝg:ℝ → ℝh:ℝx:ℝhp:Integrable (fun t => g t * Real.cosh ((x + h) * t)) μhm:Integrable (fun t => g t * Real.cosh ((x - h) * t)) μhx:Integrable (fun t => g t * Real.cosh (x * t)) μt:ℝ⊢ g t * differenceMultiplier h t * Real.cosh (x * t) =
  (((fun t => g t * Real.cosh ((x + h) * t)) + fun t => g t * Real.cosh ((x - h) * t)) - fun x_1 =>
      2 * Real.cos (h / 2) * (g x_1 * Real.cosh (x * x_1)))
    t
  have he := modifiedDifference_cosh h t xμ:Measure ℝg:ℝ → ℝh:ℝx:ℝhp:Integrable (fun t => g t * Real.cosh ((x + h) * t)) μhm:Integrable (fun t => g t * Real.cosh ((x - h) * t)) μhx:Integrable (fun t => g t * Real.cosh (x * t)) μt:ℝhe:modifiedDifference h (fun x => Real.cosh (x * t)) x = differenceMultiplier h t * Real.cosh (x * t)⊢ g t * differenceMultiplier h t * Real.cosh (x * t) =
  (((fun t => g t * Real.cosh ((x + h) * t)) + fun t => g t * Real.cosh ((x - h) * t)) - fun x_1 =>
      2 * Real.cos (h / 2) * (g x_1 * Real.cosh (x * x_1)))
    t
  dsimp [modifiedDifference] at heμ:Measure ℝg:ℝ → ℝh:ℝx:ℝhp:Integrable (fun t => g t * Real.cosh ((x + h) * t)) μhm:Integrable (fun t => g t * Real.cosh ((x - h) * t)) μhx:Integrable (fun t => g t * Real.cosh (x * t)) μt:ℝhe:Real.cosh ((x + h) * t) + Real.cosh ((x - h) * t) - 2 * Real.cos (h / 2) * Real.cosh (x * t) =
  differenceMultiplier h t * Real.cosh (x * t)⊢ g t * differenceMultiplier h t * Real.cosh (x * t) =
  (((fun t => g t * Real.cosh ((x + h) * t)) + fun t => g t * Real.cosh ((x - h) * t)) - fun x_1 =>
      2 * Real.cos (h / 2) * (g x_1 * Real.cosh (x * x_1)))
    t
  dsimpμ:Measure ℝg:ℝ → ℝh:ℝx:ℝhp:Integrable (fun t => g t * Real.cosh ((x + h) * t)) μhm:Integrable (fun t => g t * Real.cosh ((x - h) * t)) μhx:Integrable (fun t => g t * Real.cosh (x * t)) μt:ℝhe:Real.cosh ((x + h) * t) + Real.cosh ((x - h) * t) - 2 * Real.cos (h / 2) * Real.cosh (x * t) =
  differenceMultiplier h t * Real.cosh (x * t)⊢ g t * differenceMultiplier h t * Real.cosh (x * t) =
  g t * Real.cosh ((x + h) * t) + g t * Real.cosh ((x - h) * t) - 2 * Real.cos (h / 2) * (g t * Real.cosh (x * t))
  rw [mul_assoc,μ:Measure ℝg:ℝ → ℝh:ℝx:ℝhp:Integrable (fun t => g t * Real.cosh ((x + h) * t)) μhm:Integrable (fun t => g t * Real.cosh ((x - h) * t)) μhx:Integrable (fun t => g t * Real.cosh (x * t)) μt:ℝhe:Real.cosh ((x + h) * t) + Real.cosh ((x - h) * t) - 2 * Real.cos (h / 2) * Real.cosh (x * t) =
  differenceMultiplier h t * Real.cosh (x * t)⊢ g t * (differenceMultiplier h t * Real.cosh (x * t)) =
  g t * Real.cosh ((x + h) * t) + g t * Real.cosh ((x - h) * t) - 2 * Real.cos (h / 2) * (g t * Real.cosh (x * t)) ← heμ:Measure ℝg:ℝ → ℝh:ℝx:ℝhp:Integrable (fun t => g t * Real.cosh ((x + h) * t)) μhm:Integrable (fun t => g t * Real.cosh ((x - h) * t)) μhx:Integrable (fun t => g t * Real.cosh (x * t)) μt:ℝhe:Real.cosh ((x + h) * t) + Real.cosh ((x - h) * t) - 2 * Real.cos (h / 2) * Real.cosh (x * t) =
  differenceMultiplier h t * Real.cosh (x * t)⊢ g t * (Real.cosh ((x + h) * t) + Real.cosh ((x - h) * t) - 2 * Real.cos (h / 2) * Real.cosh (x * t)) =
  g t * Real.cosh ((x + h) * t) + g t * Real.cosh ((x - h) * t) - 2 * Real.cos (h / 2) * (g t * Real.cosh (x * t))]μ:Measure ℝg:ℝ → ℝh:ℝx:ℝhp:Integrable (fun t => g t * Real.cosh ((x + h) * t)) μhm:Integrable (fun t => g t * Real.cosh ((x - h) * t)) μhx:Integrable (fun t => g t * Real.cosh (x * t)) μt:ℝhe:Real.cosh ((x + h) * t) + Real.cosh ((x - h) * t) - 2 * Real.cos (h / 2) * Real.cosh (x * t) =
  differenceMultiplier h t * Real.cosh (x * t)⊢ g t * (Real.cosh ((x + h) * t) + Real.cosh ((x - h) * t) - 2 * Real.cos (h / 2) * Real.cosh (x * t)) =
  g t * Real.cosh ((x + h) * t) + g t * Real.cosh ((x - h) * t) - 2 * Real.cos (h / 2) * (g t * Real.cosh (x * t))
  ringAll goals completed! 🐙theorem abs_modifiedDifference_le (h x M : ℝ) (f : ℝ → ℝ)
    (hp : |f (x + h)| ≤ M) (hm : |f (x - h)| ≤ M)
    (hx : |f x| ≤ M) : |modifiedDifference h f x| ≤ 4 * M := byh:ℝx:ℝM:ℝf:ℝ → ℝhp:|f (x + h)| ≤ Mhm:|f (x - h)| ≤ Mhx:|f x| ≤ M⊢ |modifiedDifference h f x| ≤ 4 * M
  have hM : 0 ≤ M := (abs_nonneg _).trans hxh:ℝx:ℝM:ℝf:ℝ → ℝhp:|f (x + h)| ≤ Mhm:|f (x - h)| ≤ Mhx:|f x| ≤ MhM:0 ≤ M⊢ |modifiedDifference h f x| ≤ 4 * M
  have hc : |2 * Real.cos (h / 2) * f x| ≤ 2 * M := by
    rw [abs_mul,h:ℝx:ℝM:ℝf:ℝ → ℝhp:|f (x + h)| ≤ Mhm:|f (x - h)| ≤ Mhx:|f x| ≤ MhM:0 ≤ M⊢ |2 * Real.cos (h / 2)| * |f x| ≤ 2 * M abs_mul,h:ℝx:ℝM:ℝf:ℝ → ℝhp:|f (x + h)| ≤ Mhm:|f (x - h)| ≤ Mhx:|f x| ≤ MhM:0 ≤ M⊢ |2| * |Real.cos (h / 2)| * |f x| ≤ 2 * M abs_of_pos (byh:ℝx:ℝM:ℝf:ℝ → ℝhp:|f (x + h)| ≤ Mhm:|f (x - h)| ≤ Mhx:|f x| ≤ MhM:0 ≤ M⊢ 0 < 2 norm_numAll goals completed! 🐙 : (0 : ℝ) < 2)]h:ℝx:ℝM:ℝf:ℝ → ℝhp:|f (x + h)| ≤ Mhm:|f (x - h)| ≤ Mhx:|f x| ≤ MhM:0 ≤ M⊢ 2 * |Real.cos (h / 2)| * |f x| ≤ 2 * M
    calc
      2 * |Real.cos (h / 2)| * |f x| ≤ 2 * 1 * |f x| :=
        mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left
          (Real.abs_cos_le_one _) (byh:ℝx:ℝM:ℝf:ℝ → ℝhp:|f (x + h)| ≤ Mhm:|f (x - h)| ≤ Mhx:|f x| ≤ MhM:0 ≤ M⊢ 0 ≤ 2 norm_numAll goals completed! 🐙)) (abs_nonneg _)
      _ ≤ 2 * M := byh:ℝx:ℝM:ℝf:ℝ → ℝhp:|f (x + h)| ≤ Mhm:|f (x - h)| ≤ Mhx:|f x| ≤ MhM:0 ≤ M⊢ 2 * 1 * |f x| ≤ 2 * M nlinarithh:ℝx:ℝM:ℝf:ℝ → ℝhp:|f (x + h)| ≤ Mhm:|f (x - h)| ≤ Mhx:|f x| ≤ MhM:0 ≤ Mhc:|2 * Real.cos (h / 2) * f x| ≤ 2 * M⊢ |modifiedDifference h f x| ≤ 4 * M
  unfold modifiedDifferenceh:ℝx:ℝM:ℝf:ℝ → ℝhp:|f (x + h)| ≤ Mhm:|f (x - h)| ≤ Mhx:|f x| ≤ MhM:0 ≤ Mhc:|2 * Real.cos (h / 2) * f x| ≤ 2 * M⊢ |f (x + h) + f (x - h) - 2 * Real.cos (h / 2) * f x| ≤ 4 * M
  calc
    _ ≤ |f (x + h) + f (x - h)| + |2 * Real.cos (h / 2) * f x| :=
      abs_sub _ _
    _ ≤ (|f (x + h)| + |f (x - h)|) + |2 * Real.cos (h / 2) * f x| :=
      byh:ℝx:ℝM:ℝf:ℝ → ℝhp:|f (x + h)| ≤ Mhm:|f (x - h)| ≤ Mhx:|f x| ≤ MhM:0 ≤ Mhc:|2 * Real.cos (h / 2) * f x| ≤ 2 * M⊢ |f (x + h) + f (x - h)| + |2 * Real.cos (h / 2) * f x| ≤ |f (x + h)| + |f (x - h)| + |2 * Real.cos (h / 2) * f x| linarith [abs_add_le (f (x + h)) (f (x - h))]All goals completed! 🐙
    _ ≤ 4 * M := byh:ℝx:ℝM:ℝf:ℝ → ℝhp:|f (x + h)| ≤ Mhm:|f (x - h)| ≤ Mhx:|f x| ≤ MhM:0 ≤ Mhc:|2 * Real.cos (h / 2) * f x| ≤ 2 * M⊢ |f (x + h)| + |f (x - h)| + |2 * Real.cos (h / 2) * f x| ≤ 4 * M linarithAll goals completed! 🐙

/-- Only values within k steps of the center enter the iterated difference. -/theorem abs_iterate_modifiedDifference_le (h x M : ℝ) (f : ℝ → ℝ) (k : ℕ)
    (hf : ∀ y, |y - x| ≤ k * |h| → |f y| ≤ M) :
    |(modifiedDifference h)^[k] f x| ≤ 4 ^ k * M := byh:ℝx:ℝM:ℝf:ℝ → ℝk:ℕhf:∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M⊢ |(modifiedDifference h)^[k] f x| ≤ 4 ^ k * M
  induction k generalizing x with
  | zero =>zeroh:ℝM:ℝf:ℝ → ℝx:ℝhf:∀ (y : ℝ), |y - x| ≤ ↑0 * |h| → |f y| ≤ M⊢ |(modifiedDifference h)^[0] f x| ≤ 4 ^ 0 * M simpa using hf x (byh:ℝM:ℝf:ℝ → ℝx:ℝhf:∀ (y : ℝ), |y - x| ≤ ↑0 * |h| → |f y| ≤ M⊢ |x - x| ≤ ↑0 * |h| simpAll goals completed! 🐙)
  | succ k ih =>succh:ℝM:ℝf:ℝ → ℝk:ℕih:∀ (x : ℝ), (∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M) → |(modifiedDifference h)^[k] f x| ≤ 4 ^ k * Mx:ℝhf:∀ (y : ℝ), |y - x| ≤ ↑(k + 1) * |h| → |f y| ≤ M⊢ |(modifiedDifference h)^[k + 1] f x| ≤ 4 ^ (k + 1) * M
    rw [Function.iterate_succ_apply'succh:ℝM:ℝf:ℝ → ℝk:ℕih:∀ (x : ℝ), (∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M) → |(modifiedDifference h)^[k] f x| ≤ 4 ^ k * Mx:ℝhf:∀ (y : ℝ), |y - x| ≤ ↑(k + 1) * |h| → |f y| ≤ M⊢ |modifiedDifference h ((modifiedDifference h)^[k] f) x| ≤ 4 ^ (k + 1) * M]succh:ℝM:ℝf:ℝ → ℝk:ℕih:∀ (x : ℝ), (∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M) → |(modifiedDifference h)^[k] f x| ≤ 4 ^ k * Mx:ℝhf:∀ (y : ℝ), |y - x| ≤ ↑(k + 1) * |h| → |f y| ≤ M⊢ |modifiedDifference h ((modifiedDifference h)^[k] f) x| ≤ 4 ^ (k + 1) * M
    have bound (z : ℝ) (hz : |z - x| ≤ |h|) :
        |(modifiedDifference h)^[k] f z| ≤ 4 ^ k * M := byh:ℝx:ℝM:ℝf:ℝ → ℝk:ℕhf:∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M⊢ |(modifiedDifference h)^[k] f x| ≤ 4 ^ k * M
      apply ihh:ℝM:ℝf:ℝ → ℝk:ℕih:∀ (x : ℝ), (∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M) → |(modifiedDifference h)^[k] f x| ≤ 4 ^ k * Mx:ℝhf:∀ (y : ℝ), |y - x| ≤ ↑(k + 1) * |h| → |f y| ≤ Mz:ℝhz:|z - x| ≤ |h|⊢ ∀ (y : ℝ), |y - z| ≤ ↑k * |h| → |f y| ≤ M
      intro y hyh:ℝM:ℝf:ℝ → ℝk:ℕih:∀ (x : ℝ), (∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M) → |(modifiedDifference h)^[k] f x| ≤ 4 ^ k * Mx:ℝhf:∀ (y : ℝ), |y - x| ≤ ↑(k + 1) * |h| → |f y| ≤ Mz:ℝhz:|z - x| ≤ |h|y:ℝhy:|y - z| ≤ ↑k * |h|⊢ |f y| ≤ M
      apply hfh:ℝM:ℝf:ℝ → ℝk:ℕih:∀ (x : ℝ), (∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M) → |(modifiedDifference h)^[k] f x| ≤ 4 ^ k * Mx:ℝhf:∀ (y : ℝ), |y - x| ≤ ↑(k + 1) * |h| → |f y| ≤ Mz:ℝhz:|z - x| ≤ |h|y:ℝhy:|y - z| ≤ ↑k * |h|⊢ |y - x| ≤ ↑(k + 1) * |h|
      have ht : |y - x| ≤ |y - z| + |z - x| := byh:ℝx:ℝM:ℝf:ℝ → ℝk:ℕhf:∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M⊢ |(modifiedDifference h)^[k] f x| ≤ 4 ^ k * M
        simpa only [sub_add_sub_cancel] using abs_add_le (y - z) (z - x)h:ℝM:ℝf:ℝ → ℝk:ℕih:∀ (x : ℝ), (∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M) → |(modifiedDifference h)^[k] f x| ≤ 4 ^ k * Mx:ℝhf:∀ (y : ℝ), |y - x| ≤ ↑(k + 1) * |h| → |f y| ≤ Mz:ℝhz:|z - x| ≤ |h|y:ℝhy:|y - z| ≤ ↑k * |h|ht:|y - x| ≤ |y - z| + |z - x|⊢ |y - x| ≤ ↑(k + 1) * |h|
      push_casth:ℝM:ℝf:ℝ → ℝk:ℕih:∀ (x : ℝ), (∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M) → |(modifiedDifference h)^[k] f x| ≤ 4 ^ k * Mx:ℝhf:∀ (y : ℝ), |y - x| ≤ ↑(k + 1) * |h| → |f y| ≤ Mz:ℝhz:|z - x| ≤ |h|y:ℝhy:|y - z| ≤ ↑k * |h|ht:|y - x| ≤ |y - z| + |z - x|⊢ |y - x| ≤ (↑k + 1) * |h|
      nlinarithsucch:ℝM:ℝf:ℝ → ℝk:ℕih:∀ (x : ℝ), (∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M) → |(modifiedDifference h)^[k] f x| ≤ 4 ^ k * Mx:ℝhf:∀ (y : ℝ), |y - x| ≤ ↑(k + 1) * |h| → |f y| ≤ Mbound:∀ (z : ℝ), |z - x| ≤ |h| → |(modifiedDifference h)^[k] f z| ≤ 4 ^ k * M⊢ |modifiedDifference h ((modifiedDifference h)^[k] f) x| ≤ 4 ^ (k + 1) * M
    have hp := bound (x + h) (byh:ℝM:ℝf:ℝ → ℝk:ℕih:∀ (x : ℝ), (∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M) → |(modifiedDifference h)^[k] f x| ≤ 4 ^ k * Mx:ℝhf:∀ (y : ℝ), |y - x| ≤ ↑(k + 1) * |h| → |f y| ≤ Mbound:∀ (z : ℝ), |z - x| ≤ |h| → |(modifiedDifference h)^[k] f z| ≤ 4 ^ k * M⊢ |x + h - x| ≤ |h| simpAll goals completed! 🐙)succh:ℝM:ℝf:ℝ → ℝk:ℕih:∀ (x : ℝ), (∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M) → |(modifiedDifference h)^[k] f x| ≤ 4 ^ k * Mx:ℝhf:∀ (y : ℝ), |y - x| ≤ ↑(k + 1) * |h| → |f y| ≤ Mbound:∀ (z : ℝ), |z - x| ≤ |h| → |(modifiedDifference h)^[k] f z| ≤ 4 ^ k * Mhp:|(modifiedDifference h)^[k] f (x + h)| ≤ 4 ^ k * M⊢ |modifiedDifference h ((modifiedDifference h)^[k] f) x| ≤ 4 ^ (k + 1) * M
    have hm := bound (x - h) (byh:ℝM:ℝf:ℝ → ℝk:ℕih:∀ (x : ℝ), (∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M) → |(modifiedDifference h)^[k] f x| ≤ 4 ^ k * Mx:ℝhf:∀ (y : ℝ), |y - x| ≤ ↑(k + 1) * |h| → |f y| ≤ Mbound:∀ (z : ℝ), |z - x| ≤ |h| → |(modifiedDifference h)^[k] f z| ≤ 4 ^ k * Mhp:|(modifiedDifference h)^[k] f (x + h)| ≤ 4 ^ k * M⊢ |x - h - x| ≤ |h| simpAll goals completed! 🐙)succh:ℝM:ℝf:ℝ → ℝk:ℕih:∀ (x : ℝ), (∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M) → |(modifiedDifference h)^[k] f x| ≤ 4 ^ k * Mx:ℝhf:∀ (y : ℝ), |y - x| ≤ ↑(k + 1) * |h| → |f y| ≤ Mbound:∀ (z : ℝ), |z - x| ≤ |h| → |(modifiedDifference h)^[k] f z| ≤ 4 ^ k * Mhp:|(modifiedDifference h)^[k] f (x + h)| ≤ 4 ^ k * Mhm:|(modifiedDifference h)^[k] f (x - h)| ≤ 4 ^ k * M⊢ |modifiedDifference h ((modifiedDifference h)^[k] f) x| ≤ 4 ^ (k + 1) * M
    have hx := bound x (byh:ℝM:ℝf:ℝ → ℝk:ℕih:∀ (x : ℝ), (∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M) → |(modifiedDifference h)^[k] f x| ≤ 4 ^ k * Mx:ℝhf:∀ (y : ℝ), |y - x| ≤ ↑(k + 1) * |h| → |f y| ≤ Mbound:∀ (z : ℝ), |z - x| ≤ |h| → |(modifiedDifference h)^[k] f z| ≤ 4 ^ k * Mhp:|(modifiedDifference h)^[k] f (x + h)| ≤ 4 ^ k * Mhm:|(modifiedDifference h)^[k] f (x - h)| ≤ 4 ^ k * M⊢ |x - x| ≤ |h| simpAll goals completed! 🐙)succh:ℝM:ℝf:ℝ → ℝk:ℕih:∀ (x : ℝ), (∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M) → |(modifiedDifference h)^[k] f x| ≤ 4 ^ k * Mx:ℝhf:∀ (y : ℝ), |y - x| ≤ ↑(k + 1) * |h| → |f y| ≤ Mbound:∀ (z : ℝ), |z - x| ≤ |h| → |(modifiedDifference h)^[k] f z| ≤ 4 ^ k * Mhp:|(modifiedDifference h)^[k] f (x + h)| ≤ 4 ^ k * Mhm:|(modifiedDifference h)^[k] f (x - h)| ≤ 4 ^ k * Mhx:|(modifiedDifference h)^[k] f x| ≤ 4 ^ k * M⊢ |modifiedDifference h ((modifiedDifference h)^[k] f) x| ≤ 4 ^ (k + 1) * M
    have he := abs_modifiedDifference_le h x (4 ^ k * M)
      ((modifiedDifference h)^[k] f) hp hm hxsucch:ℝM:ℝf:ℝ → ℝk:ℕih:∀ (x : ℝ), (∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M) → |(modifiedDifference h)^[k] f x| ≤ 4 ^ k * Mx:ℝhf:∀ (y : ℝ), |y - x| ≤ ↑(k + 1) * |h| → |f y| ≤ Mbound:∀ (z : ℝ), |z - x| ≤ |h| → |(modifiedDifference h)^[k] f z| ≤ 4 ^ k * Mhp:|(modifiedDifference h)^[k] f (x + h)| ≤ 4 ^ k * Mhm:|(modifiedDifference h)^[k] f (x - h)| ≤ 4 ^ k * Mhx:|(modifiedDifference h)^[k] f x| ≤ 4 ^ k * Mhe:|modifiedDifference h ((modifiedDifference h)^[k] f) x| ≤ 4 * (4 ^ k * M)⊢ |modifiedDifference h ((modifiedDifference h)^[k] f) x| ≤ 4 ^ (k + 1) * M
    convert he using 1h:ℝM:ℝf:ℝ → ℝk:ℕih:∀ (x : ℝ), (∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M) → |(modifiedDifference h)^[k] f x| ≤ 4 ^ k * Mx:ℝhf:∀ (y : ℝ), |y - x| ≤ ↑(k + 1) * |h| → |f y| ≤ Mbound:∀ (z : ℝ), |z - x| ≤ |h| → |(modifiedDifference h)^[k] f z| ≤ 4 ^ k * Mhp:|(modifiedDifference h)^[k] f (x + h)| ≤ 4 ^ k * Mhm:|(modifiedDifference h)^[k] f (x - h)| ≤ 4 ^ k * Mhx:|(modifiedDifference h)^[k] f x| ≤ 4 ^ k * Mhe:|modifiedDifference h ((modifiedDifference h)^[k] f) x| ≤ 4 * (4 ^ k * M)⊢ 4 ^ (k + 1) * M = 4 * (4 ^ k * M)
    ringAll goals completed! 🐙