English
If the integrability hypotheses hold for hf', hfg', hfg, and HasLineDerivAt holds for f and g in the specified way, then the equality ∫ B(f x) (g' x) = − ∫ B(f' x) (g x) holds.
Русский
Если выполняются условия интегрируемости hf', hfg', hfg и HasLineDerivAt для f и g, то верно равенство интегралов.
LaTeX
$$$$ \int x\, B(f x) (g' x) \, d\mu = - \int x\, B(f' x) (g x) \, d\mu $$$$
Lean4
/-- **Integration by parts for line derivatives**
Version with a general bilinear form `B`.
If `B f g` is integrable, as well as `B f' g` and `B f g'` where `f'` and `g'` are derivatives
of `f` and `g` in a given direction `v`, then `∫ B f g' = - ∫ B f' g`. -/
theorem integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable {f f' : E → F} {g g' : E → G} {v : E}
{B : F →L[ℝ] G →L[ℝ] W} (hf'g : Integrable (fun x ↦ B (f' x) (g x)) μ)
(hfg' : Integrable (fun x ↦ B (f x) (g' x)) μ) (hfg : Integrable (fun x ↦ B (f x) (g x)) μ)
(hf : ∀ x, HasLineDerivAt ℝ f (f' x) x v) (hg : ∀ x, HasLineDerivAt ℝ g (g' x) x v) :
∫ x, B (f x) (g' x) ∂μ = -∫ x, B (f' x) (g x) ∂μ :=
by
by_cases hW : CompleteSpace W; swap
· simp [integral, hW]
rcases eq_or_ne v 0 with rfl | hv
· have Hf' x : f' x = 0 := by simpa [(hasLineDerivAt_zero (f := f) (x := x)).lineDeriv] using (hf x).lineDeriv.symm
have Hg' x : g' x = 0 := by simpa [(hasLineDerivAt_zero (f := g) (x := x)).lineDeriv] using (hg x).lineDeriv.symm
simp [Hf', Hg']
have : Nontrivial E := nontrivial_iff.2 ⟨v, 0, hv⟩
let n := finrank ℝ E
let E' := Fin (n - 1) → ℝ
obtain ⟨L, hL⟩ : ∃ L : E ≃L[ℝ] (E' × ℝ), L v = (0, 1) :=
by
have : finrank ℝ (E' × ℝ) = n := by simpa [this, E'] using Nat.sub_add_cancel finrank_pos
have L₀ : E ≃L[ℝ] (E' × ℝ) := (ContinuousLinearEquiv.ofFinrankEq this).symm
obtain ⟨M, hM⟩ : ∃ M : (E' × ℝ) ≃L[ℝ] (E' × ℝ), M (L₀ v) = (0, 1) :=
by
apply SeparatingDual.exists_continuousLinearEquiv_apply_eq
· simpa using hv
· simp
exact ⟨L₀.trans M, by simp [hM]⟩
let ν := Measure.map L μ
suffices H :
∫ (x : E' × ℝ), (B (f (L.symm x))) (g' (L.symm x)) ∂ν = -∫ (x : E' × ℝ), (B (f' (L.symm x))) (g (L.symm x)) ∂ν
by
have : μ = Measure.map L.symm ν := by simp [ν, Measure.map_map L.symm.continuous.measurable L.continuous.measurable]
have hL : IsClosedEmbedding L.symm := L.symm.toHomeomorph.isClosedEmbedding
simpa [this, hL.integral_map] using H
have L_emb : MeasurableEmbedding L := L.toHomeomorph.measurableEmbedding
apply integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2
· simpa [ν, L_emb.integrable_map_iff, Function.comp_def] using hf'g
· simpa [ν, L_emb.integrable_map_iff, Function.comp_def] using hfg'
· simpa [ν, L_emb.integrable_map_iff, Function.comp_def] using hfg
· intro x
have : f = (f ∘ L.symm) ∘ (L : E →ₗ[ℝ] (E' × ℝ)) := by ext y; simp
specialize hf (L.symm x)
rw [this] at hf
convert hf.of_comp using 1
· simp
· simp [← hL]
· intro x
have : g = (g ∘ L.symm) ∘ (L : E →ₗ[ℝ] (E' × ℝ)) := by ext y; simp
specialize hg (L.symm x)
rw [this] at hg
convert hg.of_comp using 1
· simp
· simp [← hL]
