English
For a finite index set I and a family of balanced sets U_i, the gauge on the indexed product I·π U equals the supremum over i in I of the gauges on U_i evaluated at x_i.
Русский
Для конечного множества индексов I и семейства сбалансированных множеств U_i верно: egauge 𝕜 (I.π U) x = ⨆_{i∈I} egauge 𝕜 (U_i) (x_i).
LaTeX
$$$\\forall I, U, x:\\; egauge_{\\mathbb{k}}(I.\\pi U, x) = \\big(\\bigsqcup_{i\\in I} egauge_{\\mathbb{k}}(U_i)(x_i)\\big) = \\sup_{i\\in I} egauge_{\\mathbb{k}}(U_i)(x_i).$$$
Lean4
/-- The extended gauge of a point `x` in an indexed product
with respect to a product of finitely many balanced sets `U i`, `i ∈ I`,
(and the whole spaces for the other indices)
is the supremum of the extended gauges of the components of `x`
with respect to the corresponding balanced set.
This version assumes the following technical condition:
- either `I` is the universal set;
- or one of `x i`, `i ∈ I`, is nonzero;
- or `𝕜` is nontrivially normed.
-/
theorem egauge_pi' {I : Set ι} (hI : I.Finite) {U : ∀ i, Set (E i)} (hU : ∀ i ∈ I, Balanced 𝕜 (U i)) (x : ∀ i, E i)
(hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ (𝓝[≠] (0 : 𝕜)).NeBot) :
egauge 𝕜 (I.pi U) x = ⨆ i ∈ I, egauge 𝕜 (U i) (x i) :=
by
refine le_antisymm ?_ (iSup₂_le fun i hi ↦ le_egauge_pi hi _ _)
refine le_of_forall_gt fun r hr ↦ ?_
have : ∀ i ∈ I, ∃ c : 𝕜, x i ∈ c • U i ∧ ‖c‖ₑ < r := fun i hi ↦ egauge_lt_iff.mp <| (le_iSup₂ i hi).trans_lt hr
choose! c hc hcr using this
obtain ⟨c₀, hc₀, hc₀I, hc₀r⟩ : ∃ c₀ : 𝕜, (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r :=
by
have hr₀ : 0 < r := hr.bot_lt
rcases I.eq_empty_or_nonempty with rfl | hIne
· obtain hι | hbot : IsEmpty ι ∨ (𝓝[≠] (0 : 𝕜)).NeBot := by simpa [@eq_comm _ ∅] using hI₀
· use 0
simp [@eq_comm _ ∅, hι, hr₀]
· rcases exists_enorm_lt 𝕜 hr₀.ne' with ⟨c₀, hc₀, hc₀r⟩
exact ⟨c₀, .inl hc₀, by simp, hc₀r⟩
· obtain ⟨i₀, hi₀I, hc_max⟩ : ∃ i₀ ∈ I, IsMaxOn (‖c ·‖ₑ) I i₀ := exists_max_image _ (‖c ·‖ₑ) hI hIne
by_cases H : c i₀ ≠ 0 ∨ I = univ
· exact ⟨c i₀, H, fun i hi ↦ by simpa [enorm] using hc_max hi, hcr _ hi₀I⟩
· push_neg at H
have hc0 (i : ι) (hi : i ∈ I) : c i = 0 := by simpa [H] using hc_max hi
have heg0 (i : ι) (hi : i ∈ I) : x i = 0 := zero_smul_set_subset (α := 𝕜) (U i) (hc0 i hi ▸ hc i hi)
have : (𝓝[≠] (0 : 𝕜)).NeBot := (hI₀.resolve_left H.2).resolve_left (by simpa)
rcases exists_enorm_lt 𝕜 hr₀.ne' with ⟨c₁, hc₁, hc₁r⟩
refine ⟨c₁, .inl hc₁, fun i hi ↦ ?_, hc₁r⟩
simp [hc0 i hi]
refine egauge_lt_iff.2 ⟨c₀, ?_, hc₀r⟩
rw [smul_set_pi₀' hc₀]
intro i hi
exact (hU i hi).smul_mono (hc₀I i hi) (hc i hi)
