Theory Sinc_Integral

theory Sinc_Integral
imports Distributions
(*  Title:     HOL/Probability/Sinc_Integral.thy
    Authors:   Jeremy Avigad (CMU), Luke Serafin (CMU)
    Authors:   Johannes Hölzl, TU München
*)

section ‹Integral of sinc›

theory Sinc_Integral
  imports Distributions
begin

subsection ‹Various preparatory integrals›

text ‹ Naming convention
The theorem name consists of the following parts:
  ▪ Kind of integral: ‹has_bochner_integral› / ‹integrable› / ‹LBINT›
  ▪ Interval: Interval (0 / infinity / open / closed) (infinity / open / closed)
  ▪ Name of the occurring constants: power, exp, m (for minus), scale, sin, $\ldots$
›

lemma has_bochner_integral_I0i_power_exp_m':
  "has_bochner_integral lborel (λx. x^k * exp (-x) * indicator {0 ..} x::real) (fact k)"
  using nn_intergal_power_times_exp_Ici[of k]
  by (intro has_bochner_integral_nn_integral)
     (auto simp: nn_integral_set_ennreal split: split_indicator)

lemma has_bochner_integral_I0i_power_exp_m:
  "has_bochner_integral lborel (λx. x^k * exp (-x) * indicator {0 <..} x::real) (fact k)"
  using AE_lborel_singleton[of 0]
  by (intro has_bochner_integral_cong_AE[THEN iffD1, OF _ _ _ has_bochner_integral_I0i_power_exp_m'])
     (auto split: split_indicator)

lemma integrable_I0i_exp_mscale: "0 < (u::real) ⟹ set_integrable lborel {0 <..} (λx. exp (-(x * u)))"
  using lborel_integrable_real_affine_iff[of u "λx. indicator {0 <..} x *R exp (- x)" 0]
        has_bochner_integral_I0i_power_exp_m[of 0]
  by (simp add: indicator_def zero_less_mult_iff mult_ac integrable.intros)

lemma LBINT_I0i_exp_mscale: "0 < (u::real) ⟹ LBINT x=0..∞. exp (-(x * u)) = 1 / u"
  using lborel_integral_real_affine[of u "λx. indicator {0<..} x *R exp (- x)" 0]
        has_bochner_integral_I0i_power_exp_m[of 0]
  by (auto simp: indicator_def zero_less_mult_iff interval_lebesgue_integral_0_infty field_simps
           dest!: has_bochner_integral_integral_eq)

lemma LBINT_I0c_exp_mscale_sin:
  "LBINT x=0..t. exp (-(u * x)) * sin x =
    (1 / (1 + u^2)) * (1 - exp (-(u * t)) * (u * sin t + cos t))" (is "_ = ?F t")
  unfolding zero_ereal_def
proof (subst interval_integral_FTC_finite)
  show "(?F has_vector_derivative exp (- (u * x)) * sin x) (at x within {min 0 t..max 0 t})" for x
    by (auto intro!: derivative_eq_intros
             simp: has_field_derivative_iff_has_vector_derivative[symmetric] power2_eq_square)
       (simp_all add: field_simps add_nonneg_eq_0_iff)
qed (auto intro: continuous_at_imp_continuous_on)

lemma LBINT_I0i_exp_mscale_sin:
  assumes "0 < x"
  shows "LBINT u=0..∞. ¦exp (-u * x) * sin x¦ = ¦sin x¦ / x"
proof (subst interval_integral_FTC_nonneg)
  let ?F = "λu. 1 / x * (1 - exp (- u * x)) * ¦sin x¦"
  show "⋀t. (?F has_real_derivative ¦exp (- t * x) * sin x¦) (at t)"
    using ‹0 < x› by (auto intro!: derivative_eq_intros simp: abs_mult)
  show "((?F ∘ real_of_ereal) ⤏ 0) (at_right 0)"
    using ‹0 < x› by (auto simp: zero_ereal_def ereal_tendsto_simps intro!: tendsto_eq_intros)
  have *: "((λt. exp (- t * x)) ⤏ 0) at_top"
    using ‹0 < x›
    by (auto intro!: exp_at_bot[THEN filterlim_compose] filterlim_tendsto_pos_mult_at_top filterlim_ident
             simp: filterlim_uminus_at_bot mult.commute[of _ x])
  show "((?F ∘ real_of_ereal) ⤏ ¦sin x¦ / x) (at_left ∞)"
    using ‹0 < x› unfolding ereal_tendsto_simps
    by (intro filterlim_compose[OF _ *]) (auto intro!: tendsto_eq_intros filterlim_ident)
qed auto

lemma
  shows integrable_inverse_1_plus_square:
      "set_integrable lborel (einterval (-∞) ∞) (λx. inverse (1 + x^2))"
  and LBINT_inverse_1_plus_square:
      "LBINT x=-∞..∞. inverse (1 + x^2) = pi"
proof -
  have 1: "- (pi / 2) < x ⟹ x * 2 < pi ⟹ (tan has_real_derivative 1 + (tan x)2) (at x)" for x
    using cos_gt_zero_pi[of x] by (subst tan_sec) (auto intro!: DERIV_tan simp: power_inverse)
  have 2: "- (pi / 2) < x ⟹ x * 2 < pi ⟹ isCont (λx. 1 + (tan x)2) x" for x
    using cos_gt_zero_pi[of x] by auto
  show "LBINT x=-∞..∞. inverse (1 + x^2) = pi"
    by (subst interval_integral_substitution_nonneg[of "-pi/2" "pi/2" tan "λx. 1 + (tan x)^2"])
       (auto intro: derivative_eq_intros 1 2 filterlim_tan_at_right
             simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff)
  show "set_integrable lborel (einterval (-∞) ∞) (λx. inverse (1 + x^2))"
    by (subst interval_integral_substitution_nonneg[of "-pi/2" "pi/2" tan "λx. 1 + (tan x)^2"])
       (auto intro: derivative_eq_intros 1 2 filterlim_tan_at_right
             simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff)
qed

lemma
  shows integrable_I0i_1_div_plus_square:
    "interval_lebesgue_integrable lborel 0 ∞ (λx. 1 / (1 + x^2))"
  and LBINT_I0i_1_div_plus_square:
    "LBINT x=0..∞. 1 / (1 + x^2) = pi / 2"
proof -
  have 1: "0 < x ⟹ x * 2 < pi ⟹ (tan has_real_derivative 1 + (tan x)2) (at x)" for x
    using cos_gt_zero_pi[of x] by (subst tan_sec) (auto intro!: DERIV_tan simp: power_inverse)
  have 2: "0 < x ⟹ x * 2 < pi ⟹ isCont (λx. 1 + (tan x)2) x" for x
    using cos_gt_zero_pi[of x] by auto
  show "LBINT x=0..∞. 1 / (1 + x^2) = pi / 2"
    by (subst interval_integral_substitution_nonneg[of "0" "pi/2" tan "λx. 1 + (tan x)^2"])
       (auto intro: derivative_eq_intros 1 2 tendsto_eq_intros
             simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff)
  show "interval_lebesgue_integrable lborel 0 ∞ (λx. 1 / (1 + x^2))"
    unfolding interval_lebesgue_integrable_def
    by (subst interval_integral_substitution_nonneg[of "0" "pi/2" tan "λx. 1 + (tan x)^2"])
       (auto intro: derivative_eq_intros 1 2 tendsto_eq_intros
             simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff)
qed

section ‹The sinc function, and the sine integral (Si)›

abbreviation sinc :: "real ⇒ real" where
  "sinc ≡ (λx. if x = 0 then 1 else sin x / x)"

lemma sinc_at_0: "((λx. sin x / x::real) ⤏ 1) (at 0)"
  using DERIV_sin [of 0] by (auto simp add: has_field_derivative_def field_has_derivative_at)

lemma isCont_sinc: "isCont sinc x"
proof cases
  assume "x = 0" then show ?thesis
    using LIM_equal [where g = "λx. sin x / x" and a=0 and f=sinc and l=1]
    by (auto simp: isCont_def sinc_at_0)
next
  assume "x ≠ 0" show ?thesis
    by (rule continuous_transform_within [where d = "abs x" and f = "λx. sin x / x"])
       (auto simp add: dist_real_def ‹x ≠ 0›)
qed

lemma continuous_on_sinc[continuous_intros]:
  "continuous_on S f ⟹ continuous_on S (λx. sinc (f x))"
  using continuous_on_compose[of S f sinc, OF _ continuous_at_imp_continuous_on]
  by (auto simp: isCont_sinc)

lemma borel_measurable_sinc[measurable]: "sinc ∈ borel_measurable borel"
  by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI isCont_sinc)

lemma sinc_AE: "AE x in lborel. sin x / x = sinc x"
  by (rule AE_I [where N = "{0}"], auto)

definition Si :: "real ⇒ real" where "Si t ≡ LBINT x=0..t. sin x / x"

lemma sinc_neg [simp]: "sinc (- x) = sinc x"
  by auto

(* TODO: Determine whether this can reasonably be eliminated by redefining Si. *)
lemma Si_alt_def : "Si t = LBINT x=0..t. sinc x"
proof cases
  assume "0 ≤ t" then show ?thesis
    using AE_lborel_singleton[of 0]
    by (auto simp: Si_def intro!: interval_lebesgue_integral_cong_AE)
next
  assume "¬ 0 ≤ t" then show ?thesis
    unfolding Si_def using AE_lborel_singleton[of 0]
    by (subst (1 2) interval_integral_endpoints_reverse)
       (auto simp: Si_def intro!: interval_lebesgue_integral_cong_AE)
qed

lemma Si_neg:
  assumes "T ≥ 0" shows "Si (- T) = - Si T"
proof -
  have "LBINT x=ereal 0..T. -1 *R sinc (- x) = LBINT y= ereal (- 0)..ereal (- T). sinc y"
    by (rule interval_integral_substitution_finite [OF assms])
       (auto intro: derivative_intros continuous_at_imp_continuous_on isCont_sinc)
  also have "(LBINT x=ereal 0..T. -1 *R sinc (- x)) = -(LBINT x=ereal 0..T. sinc x)"
    by (subst sinc_neg) (simp_all add: interval_lebesgue_integral_uminus)
  finally have *: "-(LBINT x=ereal 0..T. sinc x) = LBINT y= ereal 0..ereal (- T). sinc y"
    by simp
  show ?thesis
    using assms unfolding Si_alt_def
    by (subst zero_ereal_def)+ (auto simp add: * [symmetric])
qed

lemma integrable_sinc':
  "interval_lebesgue_integrable lborel (ereal 0) (ereal T) (λt. sin (t * θ) / t)"
proof -
  have *: "interval_lebesgue_integrable lborel (ereal 0) (ereal T) (λt. θ * sinc (t * θ))"
    by (intro interval_lebesgue_integrable_mult_right interval_integrable_isCont continuous_within_compose3 [OF isCont_sinc])
       auto
  show ?thesis
    by (rule interval_lebesgue_integrable_cong_AE[THEN iffD1, OF _ _ _ *])
       (insert AE_lborel_singleton[of 0], auto)
qed

(* TODO: need a better version of FTC2 *)
lemma DERIV_Si: "(Si has_real_derivative sinc x) (at x)"
proof -
  have "(at x within {min 0 (x - 1)..max 0 (x + 1)}) = at x"
    by (intro at_within_interior) auto
  moreover have "min 0 (x - 1) ≤ x" "x ≤ max 0 (x + 1)"
    by auto
  ultimately show ?thesis
    using interval_integral_FTC2[of "min 0 (x - 1)" 0 "max 0 (x + 1)" sinc x]
    by (auto simp: continuous_at_imp_continuous_on isCont_sinc Si_alt_def[abs_def] zero_ereal_def
                   has_field_derivative_iff_has_vector_derivative
             split del: if_split)
qed

lemma isCont_Si: "isCont Si x"
  using DERIV_Si by (rule DERIV_isCont)

lemma borel_measurable_Si[measurable]: "Si ∈ borel_measurable borel"
  by (auto intro: isCont_Si continuous_at_imp_continuous_on borel_measurable_continuous_on1)

lemma Si_at_top_LBINT:
  "((λt. (LBINT x=0..∞. exp (-(x * t)) * (x * sin t + cos t) / (1 + x^2))) ⤏ 0) at_top"
proof -
  let ?F = "λx t. exp (- (x * t)) * (x * sin t + cos t) / (1 + x2) :: real"
  have int: "set_integrable lborel {0<..} (λx. exp (- x) * (x + 1) :: real)"
    unfolding distrib_left
    using has_bochner_integral_I0i_power_exp_m[of 0] has_bochner_integral_I0i_power_exp_m[of 1]
    by (intro set_integral_add) (auto dest!: integrable.intros simp: ac_simps)

  have "((λt::real. LBINT x:{0<..}. ?F x t) ⤏ LBINT x::real:{0<..}. 0) at_top"
  proof (rule integral_dominated_convergence_at_top[OF _ _ int], simp_all del: abs_divide split: split_indicator)
    have *: "0 < x ⟹ ¦x * sin t + cos t¦ / (1 + x2) ≤ (x * 1 + 1) / 1" for x t :: real
      by (intro frac_le abs_triangle_ineq[THEN order_trans] add_mono)
         (auto simp add: abs_mult simp del: mult_1_right intro!: mult_mono)
    then have "1 ≤ t ⟹ 0 < x ⟹ ¦?F x t¦ ≤ exp (- x) * (x + 1)" for x t :: real
        by (auto simp add: abs_mult times_divide_eq_right[symmetric] simp del: times_divide_eq_right
                 intro!:  mult_mono)
    then show "∀F i in at_top. AE x in lborel. 0 < x ⟶ ¦?F x i¦ ≤ exp (- x) * (x + 1)"
      by (auto intro: eventually_mono eventually_ge_at_top[of "1::real"])
    show "AE x in lborel. 0 < x ⟶ (?F x ⤏ 0) at_top"
    proof (intro always_eventually impI allI)
      fix x :: real assume "0 < x"
      show "((λt. exp (- (x * t)) * (x * sin t + cos t) / (1 + x2)) ⤏ 0) at_top"
      proof (rule Lim_null_comparison)
        show "∀F t in at_top. norm (?F x t) ≤ exp (- (x * t)) * (x + 1)"
          using eventually_ge_at_top[of "1::real"] * ‹0 < x›
          by (auto simp add: abs_mult times_divide_eq_right[symmetric] simp del: times_divide_eq_right
                   intro!: mult_mono elim: eventually_mono)
        show "((λt. exp (- (x * t)) * (x + 1)) ⤏ 0) at_top"
          by (auto simp: filterlim_uminus_at_top [symmetric]
                   intro!: filterlim_tendsto_pos_mult_at_top[OF tendsto_const] ‹0<x› filterlim_ident
                           tendsto_mult_left_zero filterlim_compose[OF exp_at_bot])
      qed
    qed
  qed
  then show "((λt. (LBINT x=0..∞. exp (-(x * t)) * (x * sin t + cos t) / (1 + x^2))) ⤏ 0) at_top"
    by (simp add: interval_lebesgue_integral_0_infty)
qed

lemma Si_at_top_integrable:
  assumes "t ≥ 0"
  shows "interval_lebesgue_integrable lborel 0 ∞ (λx. exp (- (x * t)) * (x * sin t + cos t) / (1 + x2))"
  using ‹0 ≤ t› unfolding le_less
proof
  assume "0 = t" then show ?thesis
    using integrable_I0i_1_div_plus_square by simp
next
  assume [arith]: "0 < t"
  have *: "0 ≤ a ⟹ 0 < x ⟹ a / (1 + x2) ≤ a" for a x :: real
    using zero_le_power2[of x, arith] using divide_left_mono[of 1 "1+x2" a] by auto
  have "set_integrable lborel {0<..} (λx. (exp (- x) * x) * (sin t/t) + exp (- x) * cos t)"
    using has_bochner_integral_I0i_power_exp_m[of 0] has_bochner_integral_I0i_power_exp_m[of 1]
    by (intro set_integral_add set_integrable_mult_left)
       (auto dest!: integrable.intros simp: ac_simps)
  from lborel_integrable_real_affine[OF this, of t 0]
  show ?thesis
    unfolding interval_lebesgue_integral_0_infty
    by (rule Bochner_Integration.integrable_bound) (auto simp: field_simps * split: split_indicator)
qed

lemma Si_at_top: "(Si ⤏ pi / 2) at_top"
proof -
  have "∀F t in at_top. pi / 2 - (LBINT u=0..∞. exp (-(u * t)) * (u * sin t + cos t) / (1 + u^2)) = Si t"
    using eventually_ge_at_top[of 0]
  proof eventually_elim
    fix t :: real assume "t ≥ 0"
    have "Si t = LBINT x=0..t. sin x * (LBINT u=0..∞. exp (-(u * x)))"
      unfolding Si_def using ‹0 ≤ t›
      by (intro interval_integral_discrete_difference[where X="{0}"]) (auto simp: LBINT_I0i_exp_mscale)
    also have "… = LBINT x. (LBINT u=ereal 0..∞. indicator {0 <..< t} x *R sin x * exp (-(u * x)))"
      using ‹0≤t› by (simp add: zero_ereal_def interval_lebesgue_integral_le_eq mult_ac)
    also have "… = LBINT x. (LBINT u. indicator ({0<..} × {0 <..< t}) (u, x) *R (sin x * exp (-(u * x))))"
      by (subst interval_integral_Ioi) (simp_all add: indicator_times ac_simps)
    also have "… = LBINT u. (LBINT x. indicator ({0<..} × {0 <..< t}) (u, x) *R (sin x * exp (-(u * x))))"
    proof (intro lborel_pair.Fubini_integral[symmetric] lborel_pair.Fubini_integrable)
      show "(λ(x, y). indicator ({0<..} × {0<..<t}) (y, x) *R (sin x * exp (- (y * x))))
          ∈ borel_measurable (lborel ⨂M lborel)" (is "?f ∈ borel_measurable _")
        by measurable

      have "AE x in lborel. indicator {0..t} x *R abs (sinc x) = LBINT y. norm (?f (x, y))"
        using AE_lborel_singleton[of 0] AE_lborel_singleton[of t]
      proof eventually_elim
        fix x :: real assume x: "x ≠ 0" "x ≠ t"
        have "LBINT y. ¦indicator ({0<..} × {0<..<t}) (y, x) *R (sin x * exp (- (y * x)))¦ =
            LBINT y. ¦sin x¦ * exp (- (y * x)) * indicator {0<..} y * indicator {0<..<t} x"
          by (intro Bochner_Integration.integral_cong) (auto split: split_indicator simp: abs_mult)
        also have "… = ¦sin x¦ * indicator {0<..<t} x * (LBINT y=0..∞.  exp (- (y * x)))"
          by (cases "x > 0")
             (auto simp: field_simps interval_lebesgue_integral_0_infty split: split_indicator)
        also have "… = ¦sin x¦ * indicator {0<..<t} x * (1 / x)"
          by (cases "x > 0") (auto simp add: LBINT_I0i_exp_mscale)
        also have "… = indicator {0..t} x *R ¦sinc x¦"
          using x by (simp add: field_simps split: split_indicator)
        finally show "indicator {0..t} x *R abs (sinc x) = LBINT y. norm (?f (x, y))"
          by simp
      qed
      moreover have "set_integrable lborel {0 .. t} (λx. abs (sinc x))"
        by (auto intro!: borel_integrable_compact continuous_intros simp del: real_scaleR_def)
      ultimately show "integrable lborel (λx. LBINT y. norm (?f (x, y)))"
        by (rule integrable_cong_AE_imp[rotated 2]) simp

      have "0 < x ⟹ set_integrable lborel {0<..} (λy. sin x * exp (- (y * x)))" for x :: real
          by (intro set_integrable_mult_right integrable_I0i_exp_mscale)
      then show "AE x in lborel. integrable lborel (λy. ?f (x, y))"
        by (intro AE_I2) (auto simp: indicator_times split: split_indicator)
    qed
    also have "... = LBINT u=0..∞. (LBINT x=0..t. exp (-(u * x)) * sin x)"
      using ‹0≤t›
      by (auto simp: interval_lebesgue_integral_def zero_ereal_def ac_simps
               split: split_indicator intro!: Bochner_Integration.integral_cong)
    also have "… = LBINT u=0..∞. 1 / (1 + u2) - 1 / (1 + u2) * (exp (- (u * t)) * (u * sin t + cos t))"
      by (auto simp: divide_simps LBINT_I0c_exp_mscale_sin intro!: interval_integral_cong)
    also have "... = pi / 2 - (LBINT u=0..∞. exp (- (u * t)) * (u * sin t + cos t) / (1 + u^2))"
      using Si_at_top_integrable[OF ‹0≤t›] by (simp add: integrable_I0i_1_div_plus_square LBINT_I0i_1_div_plus_square)
    finally show "pi / 2 - (LBINT u=0..∞. exp (-(u * t)) * (u * sin t + cos t) / (1 + u^2)) = Si t" ..
  qed
  then show ?thesis
    by (rule Lim_transform_eventually)
       (auto intro!: tendsto_eq_intros Si_at_top_LBINT)
qed

subsection ‹The final theorems: boundedness and scalability›

lemma bounded_Si: "∃B. ∀T. ¦Si T¦ ≤ B"
proof -
  have *: "0 ≤ y ⟹ dist x y < z ⟹ abs x ≤ y + z" for x y z :: real
    by (simp add: dist_real_def)

  have "eventually (λT. dist (Si T) (pi / 2) < 1) at_top"
    using Si_at_top by (elim tendstoD) simp
  then have "eventually (λT. 0 ≤ T ∧ ¦Si T¦ ≤ pi / 2 + 1) at_top"
    using eventually_ge_at_top[of 0] by eventually_elim (insert *[of "pi/2" "Si _" 1], auto)
  then have "∃T. 0 ≤ T ∧ (∀t ≥ T. ¦Si t¦ ≤ pi / 2 + 1)"
    by (auto simp add: eventually_at_top_linorder)
  then obtain T where T: "0 ≤ T" "⋀t. t ≥ T ⟹ ¦Si t¦ ≤ pi / 2 + 1"
    by auto
  moreover have "t ≤ - T ⟹ ¦Si t¦ ≤ pi / 2 + 1" for t
    using T(1) T(2)[of "-t"] Si_neg[of "- t"] by simp
  moreover have "∃M. ∀t. -T ≤ t ∧ t ≤ T ⟶ ¦Si t¦ ≤ M"
    by (rule isCont_bounded) (auto intro!: isCont_Si continuous_intros ‹0 ≤ T›)
  then obtain M where M: "⋀t. -T ≤ t ∧ t ≤ T ⟹ ¦Si t¦ ≤ M"
    by auto
  ultimately show ?thesis
    by (intro exI[of _ "max M (pi/2 + 1)"]) (meson le_max_iff_disj linorder_not_le order_le_less)
qed

lemma LBINT_I0c_sin_scale_divide:
  assumes "T ≥ 0"
  shows "LBINT t=0..T. sin (t * θ) / t = sgn θ * Si (T * ¦θ¦)"
proof -
  { assume "0 < θ"
    have "(LBINT t=ereal 0..T. sin (t * θ) / t) = (LBINT t=ereal 0..T. θ *R sinc (t * θ))"
      by (rule interval_integral_discrete_difference[of "{0}"]) auto
    also have "… = (LBINT t=ereal (0 * θ)..T * θ. sinc t)"
      apply (rule interval_integral_substitution_finite [OF assms])
      apply (subst mult.commute, rule DERIV_subset)
      by (auto intro!: derivative_intros continuous_at_imp_continuous_on isCont_sinc)
    also have "… = (LBINT t=ereal (0 * θ)..T * θ. sin t / t)"
      by (rule interval_integral_discrete_difference[of "{0}"]) auto
    finally have "(LBINT t=ereal 0..T. sin (t * θ) / t) = (LBINT t=ereal 0..T * θ. sin t / t)"
      by simp
    hence "LBINT x. indicator {0<..<T} x * sin (x * θ) / x =
        LBINT x. indicator {0<..<T * θ} x * sin x / x"
      using assms ‹0 < θ› unfolding interval_lebesgue_integral_def einterval_eq zero_ereal_def
        by (auto simp: ac_simps)
  } note aux1 = this
  { assume "0 > θ"
    have [simp]: "integrable lborel (λx. sin (x * θ) * indicator {0<..<T} x / x)"
      using integrable_sinc' [of T θ] assms
      by (simp add: interval_lebesgue_integrable_def ac_simps)
    have "(LBINT t=ereal 0..T. sin (t * -θ) / t) = (LBINT t=ereal 0..T. -θ *R sinc (t * -θ))"
      by (rule interval_integral_discrete_difference[of "{0}"]) auto
    also have "… = (LBINT t=ereal (0 * -θ)..T * -θ. sinc t)"
      apply (rule interval_integral_substitution_finite [OF assms])
      apply (subst mult.commute, rule DERIV_subset)
      by (auto intro!: derivative_intros continuous_at_imp_continuous_on isCont_sinc)
    also have "… = (LBINT t=ereal (0 * -θ)..T * -θ. sin t / t)"
      by (rule interval_integral_discrete_difference[of "{0}"]) auto
    finally have "(LBINT t=ereal 0..T. sin (t * -θ) / t) = (LBINT t=ereal 0..T * -θ. sin t / t)"
      by simp
    hence "LBINT x. indicator {0<..<T} x * sin (x * θ) / x =
       - (LBINT x. indicator {0<..<- (T * θ)} x * sin x / x)"
      using assms ‹0 > θ› unfolding interval_lebesgue_integral_def einterval_eq zero_ereal_def
        by (auto simp add: field_simps mult_le_0_iff split: if_split_asm)
  } note aux2 = this
  show ?thesis
    using assms unfolding Si_def interval_lebesgue_integral_def sgn_real_def einterval_eq zero_ereal_def
    apply auto
    apply (erule aux1)
    apply (rule aux2)
    apply auto
    done
qed

end