English
Under integrability hypotheses, the integral of B(f x) with g' x equals the negative of the integral of B(f' x) with g x.
Русский
При условии интегрируемости интеграл от B(f x)(g' x) равен минус интеграла от B(f' x)(g x).
LaTeX
$$$$ \int x\, B(f x) (g' x) \, d\mu = - \int x\, B(f' x) (g x) \, d\mu $$$$
Lean4
theorem integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux1 [SigmaFinite μ] {f f' : E × ℝ → F}
{g g' : E × ℝ → G} {B : F →L[ℝ] G →L[ℝ] W} (hf'g : Integrable (fun x ↦ B (f' x) (g x)) (μ.prod volume))
(hfg' : Integrable (fun x ↦ B (f x) (g' x)) (μ.prod volume))
(hfg : Integrable (fun x ↦ B (f x) (g x)) (μ.prod volume)) (hf : ∀ x, HasLineDerivAt ℝ f (f' x) x (0, 1))
(hg : ∀ x, HasLineDerivAt ℝ g (g' x) x (0, 1)) :
∫ x, B (f x) (g' x) ∂(μ.prod volume) = -∫ x, B (f' x) (g x) ∂(μ.prod volume) :=
calc
∫ x, B (f x) (g' x) ∂(μ.prod volume) = ∫ x, (∫ t, B (f (x, t)) (g' (x, t))) ∂μ := integral_prod _ hfg'
_ = ∫ x, (-∫ t, B (f' (x, t)) (g (x, t))) ∂μ :=
by
apply integral_congr_ae
filter_upwards [hf'g.prod_right_ae, hfg'.prod_right_ae, hfg.prod_right_ae] with x hf'gx hfg'x hfgx
apply integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable ?_ ?_ hfg'x hf'gx hfgx
· intro t
convert (hf (x, t)).scomp_of_eq t ((hasDerivAt_id t).add (hasDerivAt_const t (-t))) (by simp) <;> simp
· intro t
convert (hg (x, t)).scomp_of_eq t ((hasDerivAt_id t).add (hasDerivAt_const t (-t))) (by simp) <;> simp
_ = -∫ x, B (f' x) (g x) ∂(μ.prod volume) := by rw [integral_neg, integral_prod _ hf'g]
