Source indexedlemma · leanprover/lean4:v4.32.0

ZetaAppendix.B1_eq_sub_nat_sub_half_of_mem_Ioo

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3016 to 3026

Mathematical statement

Exact Lean statement

lemma B1_eq_sub_nat_sub_half_of_mem_Ioo (m : ℕ) {x : ℝ}
    (hx : x ∈ Set.Ioo (m : ℝ) (m + 1 : ℝ)) :
    B1 x = x - m - 1 / 2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma B1_eq_sub_nat_sub_half_of_mem_Ioo (m : ℕ) {x : ℝ}    (hx : x ∈ Set.Ioo (m : ℝ) (m + 1 : ℝ)) :    B1 x = x - m - 1 / 2 := by  unfold B1  have hx0 : 0 ≤ x := le_trans (Nat.cast_nonneg m) hx.1.le  have hfloor : (⌊x⌋₊ : ℝ) = (m : ℝ) := by    have hfloor_int : ((⌊x⌋ : ℤ) : ℝ) = (m : ℝ) := by      simpa using        (Int.floor_eq_on_Ico' (R := ℝ) (m : ℤ) x ⟨hx.1.le, by simpa using hx.2⟩)    rw [natCast_floor_eq_intCast_floor hx0, hfloor_int]  rw [hfloor]