interval_integrable

Stream: maths

[Floris van Doorn]

Is there a good reason that docs#interval_integrable is defined the way it is? Would someone opposite if I just replace interval_integrable f a b by integrable_on f (interval_oc a b) everywhere?

[Floris van Doorn]

@Yury G. Kudryashov

[Floris van Doorn]

Also, do we actually want to use the capital iota notation for interval_oc?

[Yury G. Kudryashov]

interval_oc was not there when I defined interval_integrable.

[Yury G. Kudryashov]

Another idea: should we redefine ∫ x in a..b, f x ∂μ as sign (b - a) • ∫ x in interval_oc a b, f x ∂μ?

[Yury G. Kudryashov]

(note: I'm not going to do either of these refactors in the nearest future)

[Yury G. Kudryashov]

(though I'm going to add it as a lemma)

[Floris van Doorn]

That makes sense.

Your suggestion on how to redefine interval_integral sounds good, although it might not simplify all that much (you have to reason about scalar multiplication instead of a difference).

[Yury G. Kudryashov]

But you have 1 integral instead of 2.

[Yury G. Kudryashov]

I tried it with theorems in analysis.calculus.parametric_integral, and it works well.

[Yury G. Kudryashov]

Here is a typical proof that transfers a thm from integral to interval_integral:

begin
  simp only [interval_integrable_iff, interval_integral_eq_integral_oc,
    ← ae_restrict_iff' measurable_set_interval_oc] at *,
  have := has_deriv_at_integral_of_dominated_loc_of_deriv_le ε_pos hF_meas hF_int hF'_meas h_bound
    bound_integrable h_diff,
  exact ⟨this.1, this.2.const_smul _⟩
end

[Yury G. Kudryashov]

@Floris van Doorn Could you please have a look at #10380?