[일반] 이건 어떻게 풀어야할까

[건전여우(lustyfox2nd)]

돌겠네 그냥

[익명(223.38)]

부분적분하면 되지않나

[건전여우(lustyfox2nd)]

부분적분 했는데 적분범위가 0부터 a까지인데 분모 분자가 0이 되는 꼴이라 거기서부터 막힘

[익명(223.38)]

부분적분한다음에 절댓값 적분안으로 넣는데 (1-exp(-x))/x가 항상 1이하 양수고 감소하는거 이용하고 |f|=<1인거 쓴다음에 미적분학의 기본정리쓰면 될듯 아마

[건전여우(lustyfox2nd)]

아

[TonyMontana(thecoqproofassistant)]

a가 0 이상임?

[건전여우(lustyfox2nd)]

0보다 크니까 적분기호에서 저기에 둔게 아닐까? 일단 문제에 따로 a의 조건을 명시하진 않았지만.

[TonyMontana(thecoqproofassistant)]

f(x) := arctan x, t := 1, a := -100이면 반례가 됨.

[건전여우(lustyfox2nd)]

일단 a>0이 가정된 상황이라고 두고 합시다

[TonyMontana(thecoqproofassistant)]

a가 0 이상일 때 증명하자면, (1 - e^(- t x)) / x = int_{0}^{t}{e^-(x * y) dy}로 바꾸고, 0부터 a까지 e^-(x * y) * f'(x) * dy 적분한 게 4보다 작은 걸 보이셈.

[건전여우(lustyfox2nd)]

인테그랄 입력할때 저렇게 하는거였구나 ㄷㄷ 해볼게요 ㄱㅅㄱㅅ

[TonyMontana(thecoqproofassistant)]

부분적분을 이용하면 저게 e^-(2 * a) + 1 + e^-(2 * a) + 1보다 작다고 나와요.

[TonyMontana(thecoqproofassistant)]

"작다고"가 아니라 "작거나 같다고"라고 정정할게요

[TonyMontana(thecoqproofassistant)]

f(x) := 2 * arctan x / pi여야 반례가 되겠구나. 그나저나 푸셨어요? - PushItToTheLimit!