English
A refinement of the integration-by-parts identity for line derivatives in a real finite-dimensional setting, distributing over a Haar-measure on a product space.
Русский
Уточнение тождества интегрирования по частям для линейных производных на пространстве с мера Хаара.
LaTeX
$$$$ \text{(Real finite-dimensional setting; integrable conditions)} \Rightarrow \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_aux2 [FiniteDimensional ℝ E]
{μ : Measure (E × ℝ)} [IsAddHaarMeasure μ] {f f' : E × ℝ → F} {g g' : E × ℝ → G} {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 (0, 1))
(hg : ∀ x, HasLineDerivAt ℝ g (g' x) x (0, 1)) : ∫ x, B (f x) (g' x) ∂μ = -∫ x, B (f' x) (g x) ∂μ :=
by
let ν : Measure E := addHaar
have A : ν.prod volume = (addHaarScalarFactor (ν.prod volume) μ) • μ := isAddLeftInvariant_eq_smul _ _
have Hf'g : Integrable (fun x ↦ B (f' x) (g x)) (ν.prod volume) := by rw [A]; exact hf'g.smul_measure_nnreal
have Hfg' : Integrable (fun x ↦ B (f x) (g' x)) (ν.prod volume) := by rw [A]; exact hfg'.smul_measure_nnreal
have Hfg : Integrable (fun x ↦ B (f x) (g x)) (ν.prod volume) := by rw [A]; exact hfg.smul_measure_nnreal
rw [isAddLeftInvariant_eq_smul μ (ν.prod volume)]
simp [integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux1 Hf'g Hfg' Hfg hf hg]
