Zulip Chat Archive

Stream: maths

Topic: not integrable

Yury G. Kudryashov (Dec 07 2021 at 08:19):

Am I right that we don't have theorems of the form "these functions are not integrable on [a, b]" (e.g., x⁻¹ on [a, b] ∋ 0)?

Johan Commelin (Dec 07 2021 at 08:20):

Are you suggesting that we add counterexamples to mathlib? [shudders]
:stuck_out_tongue_wink: :rofl:

Yury G. Kudryashov (Dec 07 2021 at 08:25):

not (interval_integrable _ volume a b) is useful to prove that the integral is zero.

Yury G. Kudryashov (Dec 07 2021 at 08:26):

And formulate a lemma without an assumption 0 ∉ [a, b].

Yury G. Kudryashov (Dec 07 2021 at 08:28):

I want to prove n ≠ -1 → ∮ z in C(c, R), (z - w) ^ n = 0 where ∮ z in C(c, R), f z = ∫ θ in 0..2*π, (R * exp(θ * I) * I) • f (c + R * exp (θ * I))

Yury G. Kudryashov (Dec 07 2021 at 08:29):

In the case w ∈ metric.sphere c (|R|) ∧ n < -1, the equality follows from the fact that LHS is not integrable.

Yury G. Kudryashov (Dec 07 2021 at 08:32):

And I think that we should have something like "if f → ∞ as x → a, then f is not integrable on [a, b]".

Johan Commelin (Dec 07 2021 at 08:55):

Just to make it clear: I was of course only joking. Adding such theorems have both educational and practical value.

Sebastien Gouezel (Dec 07 2021 at 08:56):

Yury G. Kudryashov said:

And I think that we should have something like "if f → ∞ as x → a, then f is not integrable on [a, b]".

Except that this is not true (think $1/\sqrt{x}$ at $0$ ). You really need an assumption on the speed, like $1/x$ .

Yury G. Kudryashov (Dec 07 2021 at 09:14):

It was a typo: should be "f' is not integrable"

Last updated: Dec 20 2023 at 11:08 UTC