Cauchy Schwarz inequality integral form

Stream: Is there code for X?

[Jiatong Yang]

Is there code for

$$(\int_{a}^{b} fg) ^ 2 \le (\int_{a}^{b} f)^2(\int_{a}^{b} g)^2$$

[Yan Yablonovskiy]

Jiatong Yang said:

Is there code for

$$(\int_{a}^{b} fg) ^ 2 \le (\int_{a}^{b} f)^2(\int_{a}^{b} g)^2$$

Might need to be more specific as to the type of integral, since there isnt a measure or anything like that there, or what the functions go to.

[Jiatong Yang]

The simplest situation is enough:
f and g are real functions that are continuous on [a,b]

[Yan Yablonovskiy]

Jiatong Yang said:

The simplest situation is enough:
f and g are real functions that are continuous on [a,b]

Mathlib is very general, so the CS inequality will be phrased in terms of an inner product space. Perhaps
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/InnerProductSpace/Basic.html#real_inner_mul_inner_self_le

Is a start, you will also need to have that Inner Product instance(the one that does the integral)

I think there is a Holder inequality using integral notation though, integral_mul_norm_le_Lp_mul_Lq could help

[Kalle Kytölä]

Indeed a combination of docs#norm_inner_le_norm and docs#MeasureTheory.L2.innerProductSpace essentially give the correct version of Cauchy-Schwarz for integrals. (In your example case of continuous functions on $[a,b]$, docs#BoundedContinuousFunction.mem_Lp with the finite measure given by the restriction of the Lebesgue measure on $[a,b]$ gives the $L^2$-membership.) Note, however, that the inequality you stated in the original question is not true; the squares on the RHS should be on the functions inside the integrals, not on the integrals.

[Yan Yablonovskiy]

docs#MeasureTheory.integral_mul_norm_le_Lp_mul_Lq could also help, depending on what you need integral CS for.

[Jiatong Yang]

Thanks for so much help!! :smiley: