ZetaAppendix.secondIBPExpr_eq_negB1IntegralExpr

lemma secondIBPExpr_eq_negB1IntegralExpr {a b : ℝ} (ha : 0 < a) (hab : a ≤ b)    (s : ℂ) :    secondIBPExpr s a b = negB1IntegralExpr s a b := by  let P : ℕ → Prop := fun d ↦    ∀ {a b : ℝ}, 0 < a → a ≤ b → ⌊b⌋₊ - ⌊a⌋₊ = d →      secondIBPExpr s a b = negB1IntegralExpr s a b  have hP : ∀ d, P d := by    intro d    induction d using Nat.strong_induction_on with    | h d ih =>        intro a b ha hab hd        by_cases hfloor_eq : ⌊b⌋₊ = ⌊a⌋₊        · let m : ℕ := ⌊a⌋₊          have hmu : (m : ℝ) ≤ a := by            simpa [m] using Nat.floor_le (le_of_lt ha)          have hb_nonneg : 0 ≤ b := le_trans (le_of_lt ha) hab          have hvm : b ≤ (m + 1 : ℝ) := by            have hb_lt : b < (⌊b⌋₊ : ℝ) + 1 := Nat.lt_floor_add_one b            have hcast : (⌊b⌋₊ : ℝ) = (m : ℝ) := by              simp [m, hfloor_eq]            linarith          exact secondIBPExpr_eq_negB1_on_unit hab ha m hmu hvm s        · have hfloor_le : ⌊a⌋₊ ≤ ⌊b⌋₊ := Nat.floor_mono hab          have hfloor_lt : ⌊a⌋₊ < ⌊b⌋₊ := by            exact lt_of_le_of_ne hfloor_le (fun h ↦ hfloor_eq h.symm)          let c : ℝ := ((⌊a⌋₊ + 1 : ℕ) : ℝ)          have hac : a ≤ c := by            exact le_of_lt (by simpa [c] using Nat.lt_floor_add_one a)          have hcb : c ≤ b := by            have hb_nonneg : 0 ≤ b := le_trans (le_of_lt ha) hab            have hfloor_b_le : (⌊b⌋₊ : ℝ) ≤ b := Nat.floor_le hb_nonneg            have hsucc_le_nat : ⌊a⌋₊ + 1 ≤ ⌊b⌋₊ := Nat.succ_le_iff.mpr hfloor_lt            have hsucc_le : (((⌊a⌋₊ + 1 : ℕ) : ℝ)) ≤ (⌊b⌋₊ : ℝ) := by              exact_mod_cast hsucc_le_nat            exact le_trans (by simpa [c] using hsucc_le) hfloor_b_le          have hc_pos : 0 < c := lt_of_lt_of_le ha hac          have hlocal : secondIBPExpr s a c = negB1IntegralExpr s a c := by            refine secondIBPExpr_eq_negB1_on_unit hac ha ⌊a⌋₊ ?_ ?_ s            · exact Nat.floor_le (le_of_lt ha)            · simp [c]          have hfloor_c : ⌊c⌋₊ = ⌊a⌋₊ + 1 := by            simpa [c] using (Nat.floor_natCast (⌊a⌋₊ + 1))          have hsmaller : ⌊b⌋₊ - ⌊c⌋₊ < d := by            rw [hfloor_c]            omega          have hrec : secondIBPExpr s c b = negB1IntegralExpr s c b := by            exact ih (⌊b⌋₊ - ⌊c⌋₊) hsmaller hc_pos hcb rfl          calc            secondIBPExpr s a b                = secondIBPExpr s a c + secondIBPExpr s c b := by                    exact (secondIBPExpr_add_adjacent hac hcb ha s).symm            _ = negB1IntegralExpr s a c + negB1IntegralExpr s c b := by                    rw [hlocal, hrec]            _ = negB1IntegralExpr s a b := negB1IntegralExpr_add_adjacent hac hcb ha s  exact hP (⌊b⌋₊ - ⌊a⌋₊) ha hab rfl