English
Given a map f : E [⋀^ι]→ₗ[𝕜] (F [⋀^ι']→ₗ[𝕜] G) and a bound C with H, we can upgrade all Alt maps in the domain to continuous alternating maps, producing a map mkContinuousAlternating f C H : E [⋀^ι]→L[𝕜] (F [⋀^ι']→L[𝕜] G) with norm controlled by max(C,0).
Русский
Задано отображение f в чередующих многомерных пространственных переменных; при наличии соответствующего оценочного неравенства можно перейти к отображению mkContinuousAlternating, являющемуся непрерывным чередующим отображением, и контролировать его норму максимумом из C и 0.
LaTeX
$$$\\\\| mkContinuousAlternating f C H \\\\| \\\\le \\\\ max(C, 0),$ где $H$ обеспечивает неравенство $\\\\|f m_1 m_2\\\\| \\\\le (C \\\\prod_i \\\\|m_{1,i}\\\\|) \\\\prod_i \\\\|m_{2,i}\\\\|$ для всех $m_1,m_2$.$$
Lean4
/-- Given a map `f : E [⋀^ι]→ₗ[𝕜] (F [⋀^ι']→ₗ[𝕜] G)` and an estimate
`H : ∀ m m', ‖f m m'‖ ≤ C * ∏ i, ‖m i‖ * ∏ i, ‖m' i‖`, upgrade all `AlternatingMap`s in the type
to `ContinuousAlternatingMap`s. -/
def mkContinuousAlternating (f : E [⋀^ι]→ₗ[𝕜] (F [⋀^ι']→ₗ[𝕜] G)) (C : ℝ)
(H : ∀ m₁ m₂, ‖f m₁ m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) : E [⋀^ι]→L[𝕜] (F [⋀^ι']→L[𝕜] G) :=
mkContinuous
{ toFun m := mkContinuous (f m) (C * ∏ i, ‖m i‖) <| H m
map_update_add' m i x y := by ext1; simp
map_update_smul' m i c x := by ext1; simp
map_eq_zero_of_eq' v i j hv
hij := by
ext v'
have : f v = 0 := by simpa using f.map_eq_zero_of_eq' v i j hv hij
simp [this] }
(max C 0) fun m => by
simp only [coe_mk, MultilinearMap.coe_mk]
refine ((f m).mkContinuous_norm_le' _).trans_eq ?_
rw [max_mul_of_nonneg, zero_mul]
positivity
