1-\epsilon method

Stream: maths

[Junqi Liu]

How to use 1-$\epsilon$ method to prove integral equations. For example, if I want to prove $\int_ 0^1 f(x)dx$, I want to show the integral equals to $\lim_{\epsilon \rightarrow 0} \int_0^{1-\epsilon} f(x) dx$, what should I do?

[Adam Topaz]

please wrap latex in double-$. E.g. $$a + b$$ gives $a+b$

[Junqi Liu]

Adam Topaz said:

+

ok! I'm so sorry!
How to use 1-$\epsilon$ method to prove integral equations. For example, if I want to prove $\int_ 0^1 f(x)dx$, I want to show the integral equals to $\lim_{\epsilon \rightarrow 0} \int_0^{1-\epsilon} f(x) dx$, what should I do?

[Yury G. Kudryashov]

This channel is for questions about the language, not math library. Please move this thread to #maths or new members

[Yury G. Kudryashov]

@loogle intervalIntegral, Filter.Tendsto

[loogle]

:search: intervalIntegral.tendsto_integral_filter_of_dominated_convergence, intervalIntegral.integral_hasDerivAt_of_tendsto_ae_right, and 44 more

[Yury G. Kudryashov]

@loogle intervalIntegral, ContinuousWithinAt

[loogle]

:search: intervalIntegral.continuousWithinAt_primitive, intervalIntegral.continuousWithinAt_of_dominated_interval, and 4 more

[Yury G. Kudryashov]

First hit in the second search gives you continuity of the integral with respect to b.

[Notification Bot]

This topic was moved here from #lean4 > 1-\epsilion method by Kyle Miller.