Source indexedtheorem · leanprover/lean4:v4.32.0

local_quotient_eq_dslope

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:487 to 508

Mathematical statement

Exact Lean statement

theorem local_quotient_eq_dslope
    (f : ℝ → E) (x : ℝ) {u : ℝ} (hu : u ≠ 0) :
    ((-1 / π : ℂ) • dslope f x (x - u)) =
      (if u = 0 then 0 else (1 / (π * u) : ℂ) • (f (x - u) - f x))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem local_quotient_eq_dslope    (f : ℝ → E) (x : ℝ) {u : ℝ} (hu : u ≠ 0) :    ((-1 / π : ℂ) • dslope f x (x - u)) =      (if u = 0 then 0 else (1 / (π * u) : ℂ) • (f (x - u) - f x)) := by  rw [if_neg hu]  have hne : x - u ≠ x := by    intro h    have : u = 0 := by linarith    exact hu this  rw [dslope_of_ne f hne]  rw [slope_def_module]  let r : ℝ := (x - u - x)⁻¹  change (-1 / π : ℂ) • (r • (f (x - u) - f x)) =    (1 / (π * u) : ℂ) • (f (x - u) - f x)  rw [← smul_comm r ((-1 / π : ℂ))]  rw [RCLike.real_smul_eq_coe_smul (K := ℂ) (E := E)]  rw [← smul_assoc]  congr 1  dsimp [r]  push_cast  field_simp [hu, Real.pi_ne_zero]  ring