LeanPool.SardMoreira.ContinuousMultilinearMap #
theorem
ContinuousMultilinearMap.prod_add_prod
{ι : Type u_1}
{R : Type u_2}
{E : ι → Type u_3}
{F : Type u_4}
{G : Type u_5}
[Semiring R]
[(i : ι) → AddCommMonoid (E i)]
[(i : ι) → Module R (E i)]
[(i : ι) → TopologicalSpace (E i)]
[AddCommMonoid F]
[Module R F]
[TopologicalSpace F]
[AddCommMonoid G]
[Module R G]
[TopologicalSpace G]
[ContinuousAdd F]
[ContinuousAdd G]
(f₁ f₂ : ContinuousMultilinearMap R E F)
(g₁ g₂ : ContinuousMultilinearMap R E G)
:
theorem
ContinuousMultilinearMap.compContinuousLinearMap_sum_left
{ι : Type u_1}
{R : Type u_2}
{E : ι → Type u_3}
{F : Type u_4}
[Semiring R]
[(i : ι) → AddCommMonoid (E i)]
[(i : ι) → Module R (E i)]
[(i : ι) → TopologicalSpace (E i)]
[AddCommMonoid F]
[Module R F]
[TopologicalSpace F]
{E' : ι → Type u_6}
[(i : ι) → AddCommMonoid (E' i)]
[(i : ι) → Module R (E' i)]
[(i : ι) → TopologicalSpace (E' i)]
[ContinuousAdd F]
{ι' : Type u_7}
(s : Finset ι')
(f : ι' → ContinuousMultilinearMap R E F)
(g : (i : ι) → E' i →L[R] E i)
:
theorem
ContinuousMultilinearMap.prod_sub_prod
{ι : Type u_1}
{R : Type u_2}
{E : ι → Type u_3}
{F : Type u_4}
{G : Type u_5}
[Ring R]
[(i : ι) → AddCommGroup (E i)]
[(i : ι) → Module R (E i)]
[(i : ι) → TopologicalSpace (E i)]
[AddCommGroup F]
[Module R F]
[TopologicalSpace F]
[AddCommGroup G]
[Module R G]
[TopologicalSpace G]
[IsTopologicalAddGroup F]
[IsTopologicalAddGroup G]
(f₁ f₂ : ContinuousMultilinearMap R E F)
(g₁ g₂ : ContinuousMultilinearMap R E G)
:
@[simp]
theorem
ContinuousMultilinearMap.compContinuousLinearMap_neg_left
{ι : Type u_1}
{R : Type u_2}
{E : ι → Type u_3}
{F : Type u_4}
[Ring R]
[(i : ι) → AddCommGroup (E i)]
[(i : ι) → Module R (E i)]
[(i : ι) → TopologicalSpace (E i)]
[AddCommGroup F]
[Module R F]
[TopologicalSpace F]
{E' : ι → Type u_6}
[(i : ι) → AddCommGroup (E' i)]
[(i : ι) → Module R (E' i)]
[(i : ι) → TopologicalSpace (E' i)]
[IsTopologicalAddGroup F]
(f : ContinuousMultilinearMap R E F)
(g : (i : ι) → E' i →L[R] E i)
:
theorem
ContinuousMultilinearMap.compContinuousLinearMap_sub
{ι : Type u_1}
{R : Type u_2}
{E : ι → Type u_3}
{F : Type u_4}
[Ring R]
[(i : ι) → AddCommGroup (E i)]
[(i : ι) → Module R (E i)]
[(i : ι) → TopologicalSpace (E i)]
[AddCommGroup F]
[Module R F]
[TopologicalSpace F]
{E' : ι → Type u_6}
[(i : ι) → AddCommGroup (E' i)]
[(i : ι) → Module R (E' i)]
[(i : ι) → TopologicalSpace (E' i)]
[IsTopologicalAddGroup F]
(f g : ContinuousMultilinearMap R E F)
(h : (i : ι) → E' i →L[R] E i)
:
theorem
ContinuousMultilinearMap.const_apply_sub_const_apply_isBigO
{ι : Type u_1}
{α : Type u_2}
{𝕜 : Type u_3}
{E : ι → Type u_4}
{G : Type u_6}
{H : Type u_7}
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup H]
[Finite ι]
(f : ContinuousMultilinearMap 𝕜 E G)
{g₁ g₂ : α → (i : ι) → E i}
{B : α → H}
{l : Filter α}
(hg₁ : ∀ (i : ι), Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖g₁ x i‖)
(hg₂ : ∀ (i : ι), Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖g₂ x i‖)
(hsub : ∀ (i : ι), (fun (a : α) => g₁ a i - g₂ a i) =O[l] B)
:
@[simp]
theorem
ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear_apply
{ι : Type u_1}
{𝕜 : Type u_3}
{E : ι → Type u_4}
{F : ι → Type u_5}
{G : Type u_6}
[NontriviallyNormedField 𝕜]
[Fintype ι]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[(i : ι) → NormedAddCommGroup (F i)]
[(i : ι) → NormedSpace 𝕜 (F i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(f : (i : ι) → E i →L[𝕜] F i)
:
theorem
ContinuousMultilinearMap.compContinuousLinearMap_sub_compContinuousLinearMap_isBigO
{ι : Type u_1}
{α : Type u_2}
{𝕜 : Type u_3}
{E : ι → Type u_4}
{F : ι → Type u_5}
{G : Type u_6}
{H : Type u_7}
[NontriviallyNormedField 𝕜]
[Fintype ι]
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[(i : ι) → NormedAddCommGroup (F i)]
[(i : ι) → NormedSpace 𝕜 (F i)]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup H]
{f₁ f₂ : α → ContinuousMultilinearMap 𝕜 F G}
{g₁ g₂ : α → (i : ι) → E i →L[𝕜] F i}
{l : Filter α}
{B : α → H}
(hf₂_bdd : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖f₂ x‖)
(hf_sub : (fun (a : α) => f₁ a - f₂ a) =O[l] B)
(hg₁_bdd : ∀ (i : ι), Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖g₁ x i‖)
(hg₂_bdd : ∀ (i : ι), Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖g₂ x i‖)
(hg_sub : ∀ (i : ι), (fun (a : α) => g₁ a i - g₂ a i) =O[l] B)
:
(fun (a : α) => (f₁ a).compContinuousLinearMap (g₁ a) - (f₂ a).compContinuousLinearMap (g₂ a)) =O[l] B