English
The map g ↦ mulInvariantVectorField v g is ContMDiff of minimal smoothness; the construction is smooth in g.
Русский
Отображение g ↦ mulInvariantVectorField v g гладко по g в минимальной степени гладкости.
LaTeX
$$ContMDiff I I.tangent (minSmoothness 𝕜 2) (fun g => (mulInvariantVectorField v g))$$
Lean4
@[to_additive (attr := simp)]
theorem inverse_mfderiv_mul_left {g h : G} :
(mfderiv I I (fun b ↦ g * b) h).inverse = mfderiv I I (fun b ↦ g⁻¹ * b) (g * h) :=
by
have M : 1 ≤ minSmoothness 𝕜 3 := le_trans (by simp) le_minSmoothness
have A : mfderiv I I ((fun x ↦ g⁻¹ * x) ∘ (fun x ↦ g * x)) h = ContinuousLinearMap.id _ _ :=
by
have : (fun x ↦ g⁻¹ * x) ∘ (fun x ↦ g * x) = id := by ext x; simp
rw [this, id_eq, mfderiv_id]
rw [mfderiv_comp (I' := I) _ (contMDiff_mul_left.contMDiffAt.mdifferentiableAt M)
(contMDiff_mul_left.contMDiffAt.mdifferentiableAt M)] at A
have A' : mfderiv I I ((fun x ↦ g * x) ∘ (fun x ↦ g⁻¹ * x)) (g * h) = ContinuousLinearMap.id _ _ :=
by
have : (fun x ↦ g * x) ∘ (fun x ↦ g⁻¹ * x) = id := by ext x; simp
rw [this, id_eq, mfderiv_id]
rw [mfderiv_comp (I' := I) _ (contMDiff_mul_left.contMDiffAt.mdifferentiableAt M)
(contMDiff_mul_left.contMDiffAt.mdifferentiableAt M),
inv_mul_cancel_left g h] at A'
exact ContinuousLinearMap.inverse_eq A' A
