Theory Examples_Integral

theory
Examples_Integral
imports
  "HOL-ODE-Numerics.ODE_Numerics"
begin

text ‹Examples taken from Mahboubi, Sibut-Pinote: Formally Verified Approximations of Definite Integrals.
  🌐‹https://link.springer.com/chapter/10.1007/978-3-319-43144-4_17››

lemma mk_ode_ops_ne_None: "mk_ode_ops e f ≠ None"
  if "max_Var_floatariths e ≤ length e"
    "open_form f"
    "max_Var_form f ≤ length e"
  using that
  including ode_ops.lifting
  by transfer auto

subsection ‹Example 1›

lemma ex1_3: "¦integral {0 .. 1} (λx. 1 / (1 + x*x::real)) - pi/4¦ ≤ 1 / 10^3"
  by (rule abs_minus_leI) (tactic ‹integral_bnds_tac 1 30 5 6 13 "-" [] @{context} 1›)

lemma ex1_6: "¦integral {0 .. 1} (λx. 1 / (1 + x*x::real)) - pi/4¦ ≤ 1 / 10^6"
  by (rule abs_minus_leI) (tactic ‹integral_bnds_tac 1 30 5 6 25 "" [] @{context} 1›)

lemma ex1_9: "¦integral {0 .. 1} (λx. 1 / (1 + x*x::real)) - pi/4¦ ≤ 1 / 10^9"
  by (rule abs_minus_leI) (tactic ‹integral_bnds_tac 1 50 5 6 40 "" [] @{context} 1›)


subsection ‹Example 2›

lemma add_nonneg_pos_ne_zero: "a ≥ 0 ⟹ b > 0 ⟹ a + b ≠ 0" for a b::real by arith
lemmas pow_gt_zero = add_nonneg_pos add_nonneg_pos_ne_zero

lemma ex2_3: "¦integral {0 .. 1} (λx::real. arctan (sqrt (x⇧2 + 2)) / (sqrt (x⇧2 + 2) * (x⇧2 + 1))) - 5*pi⇧2/96¦ ≤ 1 / 10^3"
  by (rule abs_minus_leI) (tactic ‹integral_bnds_tac 1 30 10 6 12 "" @{thms pow_gt_zero} @{context} 1›)

lemma ex2_6: "¦integral {0 .. 1} (λx::real. arctan (sqrt (x⇧2 + 2)) / (sqrt (x⇧2 + 2) * (x⇧2 + 1))) - 5*pi⇧2/96¦ ≤ 1 / 10^6"
  by (rule abs_minus_leI) (tactic ‹integral_bnds_tac 1 40 10 6 26 "" @{thms pow_gt_zero} @{context} 1›)


subsection ‹Example 3›

lemma pi_bounds_nonneg[simp]: "0 ≤ real_of_float (ub_pi p)"
  using pi_boundaries[of p]
  by (auto intro: pi_ge_zero[le])

lemma ex3_3: "¦integral {0 .. pi} (λx::real. (x * sin x) / (1 + (cos x)⇧2)) - pi⇧2/4¦ ≤ 1 / 10^3"
  by (rule abs_minus_leI) (tactic ‹integral_bnds_tac 1 30 10 6 15 "" [] @{context} 1›)

lemma ex3_6: "¦integral {0 .. pi} (λx::real. (x * sin x) / (1 + (cos x)⇧2)) - pi⇧2/4¦ ≤ 1 / 10^6"
  by (rule abs_minus_leI) (tactic ‹integral_bnds_tac 1 40 10 6 30 "" [] @{context} 1›)


subsection ‹Example 4›

text ‹Absolute Value...›


subsection ‹Example 5›

lemma
  "¦integral {-1 .. 1} (λx::real. (2048*x^12 - 6144*x^10 + 6912*x^8 - 3584*x^6 + 840*x^4 - 72*x⇧2 +1) *
      exp (-((x - 3/4)⇧2)) * sqrt(1 - x⇧2)) -
    real_divl 80 (-32555895745) (10^16)¦ ≤ 1 / 10^1"
  oops

text ‹@{term "sqrt(1 - x⇧2)"} not differentiable @{term "at 0"}›

subsection ‹Example 6›

lemma
  "¦integral {0 .. 8} (λx::real. sin (x + exp x)) - 0.3474¦ ≤ 1 / 10^1"
  by (rule abs_minus_leI) (tactic ‹integral_bnds_tac 1 40 3 6 15 "" [] @{context} 1›)― ‹slow: 700s›

lemma
  "¦integral {0 .. 8} (λx::real. sin (x + exp x)) - 0.3474¦ ≤ 1 / 10^2"
  oops (*
  by (rule abs_minus_leI) (tactic ‹integral_bnds_tac 1 40 3 6 20 "" @{context} 1›) *)

end