Source indexedlemma · leanprover/lean4:v4.32.0

ZetaAppendix.continuous_bernoulli2_primitive

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3062 to 3073

Mathematical statement

Exact Lean statement

lemma continuous_bernoulli2_primitive :
    Continuous
      (fun y : ℝ ↦
        (((-(Int.fract y ^ 2 - Int.fract y + 1 / 6) / 2) : ℝ) : ℂ))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma continuous_bernoulli2_primitive :    Continuous      (fun y : ℝ ↦        (((-(Int.fract y ^ 2 - Int.fract y + 1 / 6) / 2) : ℝ) : ℂ)) := by  let p : ℝ → ℂ := fun x ↦ (((-(x ^ 2 - x + 1 / 6) / 2) : ℝ) : ℂ)  have hp_cont : ContinuousOn p (Set.Icc (0 : ℝ) 1) := by    simp only [one_div, neg_add_rev, neg_sub, ofReal_div, ofReal_add, ofReal_neg, ofReal_inv,      ofReal_ofNat, ofReal_sub, ofReal_pow, p]    fun_prop  have hp_end : p 0 = p 1 := by    norm_num [p]  simpa [p, Function.comp_def] using hp_cont.comp_fract'' hp_end