English
The underlying function of the continuous multilinear extension equals the original multilinear map on the universal coordinates.
Русский
Основа функция непрерывной многообразной продолжения совпадает с исходной многообразной картой на общем наборе координат.
LaTeX
$$⇑(f.mkContinuous C H) = f$$
Lean4
/-- If a multilinear map `f` satisfies a boundedness property around `0`,
one can deduce a bound on `f m₁ - f m₂` using the multilinearity.
Here, we give a precise but hard to use version.
See `norm_image_sub_le_of_bound` for a less precise but more usable version.
The bound reads
`‖f m - f m'‖ ≤
C * ‖m 1 - m' 1‖ * max ‖m 2‖ ‖m' 2‖ * max ‖m 3‖ ‖m' 3‖ * ... * max ‖m n‖ ‖m' n‖ + ...`,
where the other terms in the sum are the same products where `1` is replaced by any `i`. -/
theorem norm_image_sub_le_of_bound' [DecidableEq ι] (f : MultilinearMap 𝕜 E G) {C : ℝ} (hC : 0 ≤ C)
(H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) (m₁ m₂ : ∀ i, E i) :
‖f m₁ - f m₂‖ ≤ C * ∑ i, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ :=
by
have A :
∀ s : Finset ι,
‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ :=
fun s ↦ by
induction s using Finset.induction with
| empty => simp
| insert i s his
Hrec =>
have I :
‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ ≤
C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ :=
by
have A : (insert i s).piecewise m₂ m₁ = Function.update (s.piecewise m₂ m₁) i (m₂ i) := s.piecewise_insert _ _ _
have B : s.piecewise m₂ m₁ = Function.update (s.piecewise m₂ m₁) i (m₁ i) := by simp [his]
rw [B, A, ← f.map_update_sub]
apply le_trans (H _)
gcongr with j
by_cases h : j = i
· rw [h]
simp
· by_cases h' : j ∈ s <;> simp [h', h]
calc
‖f m₁ - f ((insert i s).piecewise m₂ m₁)‖ ≤
‖f m₁ - f (s.piecewise m₂ m₁)‖ + ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ :=
by
rw [← dist_eq_norm, ← dist_eq_norm, ← dist_eq_norm]
exact dist_triangle _ _ _
_ ≤
(C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) +
C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ :=
(add_le_add Hrec I)
_ = C * ∑ i ∈ insert i s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ := by
simp [his, add_comm, left_distrib]
convert A univ
simp
