norm_mul_le_const_mul_norm — Mathlib

English

There exists a positive constant c such that ∀ x,y ∈ L, B.norm(xy) ≤ c · B.norm x · B.norm y, assuming B i = 1 for some i and the K-norm is nonarchimedean.

Русский

Существует некоторое положительное число c such that для всех x,y ∈ L выполняется B.norm(xy) ≤ c B.norm(x) B.norm(y).

LaTeX

$$$\exists c>0\; \forall x,y\in L,\ B.norm(xy) \le c \cdot B.norm(x) \cdot B.norm(y)$$$

Lean4

/-- For any `K`-basis of `L`, `B.norm` is bounded with respect to multiplication. That is,
  `∃ (c : ℝ), c > 0` such that ` ∀ (x y : L), B.norm (x * y) ≤ c * B.norm x * B.norm y`. -/
theorem norm_mul_le_const_mul_norm {i : ι} (hBi : B i = (1 : L)) (hna : IsNonarchimedean (Norm.norm : K → ℝ)) :
    ∃ (c : ℝ) (_ : 0 < c), ∀ x y : L, B.norm (x * y) ≤ c * B.norm x * B.norm y := by
  -- The bounding constant `c` will be the maximum of the products `B.norm (B i * B j)`.

  obtain ⟨c, _, hc⟩ := exists_mem_eq_sup' univ_nonempty (fun i : ι × ι ↦ B.norm (B i.1 * B i.2))
  use B.norm (B c.1 * B c.2)
  constructor
    -- ∀ (x y : L), B.norm (x * y) ≤ B.norm (⇑B c.fst * ⇑B c.snd) * B.norm x * B.norm y

  · intro x y
    obtain ⟨ixy, _, hixy_def⟩ :=
      exists_mem_eq_sup' univ_nonempty
        (fun i ↦ ‖(B.repr (x * y)) i‖)
          -- We rewrite the LHS using `ixy`.

    conv_lhs => simp only [Basis.norm]; rw [hixy_def, ← Basis.sum_repr B x, ← Basis.sum_repr B y]
    rw [sum_mul, map_finset_sum]
    simp_rw [smul_mul_assoc, LinearEquiv.map_smul, mul_sum, map_finset_sum, mul_smul_comm, LinearEquiv.map_smul]
    have hna' : IsNonarchimedean (NormedField.toMulRingNorm K) := hna
    obtain
      ⟨k, -,
        (hk :
          ‖∑ i : ι, (B.repr x i • ∑ i_1 : ι, B.repr y i_1 • B.repr (B i * B i_1)) ixy‖ ≤
            ‖(B.repr x k • ∑ j : ι, B.repr y j • B.repr (B k * B j)) ixy‖)⟩ :=
      IsNonarchimedean.finset_image_add hna' (fun i ↦ (B.repr x i • ∑ i_1 : ι, B.repr y i_1 • B.repr (B i * B i_1)) ixy)
        (univ : Finset ι)
    simp only [Finsupp.coe_smul, Finsupp.coe_finset_sum, Pi.smul_apply, sum_apply, smul_eq_mul, norm_mul] at hk ⊢
    apply le_trans hk
    obtain ⟨k', hk'⟩ :
      ∃ (k' : ι), ‖∑ j : ι, B.repr y j • B.repr (B k * B j) ixy‖ ≤ ‖B.repr y k' • B.repr (B k * B k') ixy‖ :=
      by
      obtain ⟨k, hk0, hk⟩ :=
        IsNonarchimedean.finset_image_add hna' (fun i ↦ B.repr y i • B.repr (B k * B i) ixy) (univ : Finset ι)
      exact ⟨k, hk⟩
    apply
      le_trans
        (mul_le_mul_of_nonneg_left hk' (norm_nonneg _))
          -- Now an easy computation leads to the desired conclusion.

    rw [norm_smul, mul_assoc, mul_comm (B.norm (B c.fst * B c.snd)), ← mul_assoc]
    exact
      mul_le_mul (mul_le_mul (B.norm_repr_le_norm _) (B.norm_repr_le_norm _) (norm_nonneg _) (B.norm_nonneg _))
        (le_trans (B.norm_repr_le_norm _)
          (hc ▸ Finset.le_sup' (fun i : ι × ι ↦ B.norm (B i.1 * B i.2)) (mem_univ (k, k'))))
        (norm_nonneg _)
        (mul_nonneg (B.norm_nonneg _) (B.norm_nonneg _))
          -- `B c.1 * B c.2` is positive.

  · have h_pos : (0 : ℝ) < B.norm (B i * B i) :=
      by
      have h1 : (1 : L) = (algebraMap K L) 1 := by rw [map_one]
      rw [hBi, mul_one, h1, Basis.norm_extends hBi]
      simp [norm_one, zero_lt_one]
    exact lt_of_lt_of_le h_pos (hc ▸ Finset.le_sup' (fun i : ι × ι ↦ B.norm (B i.1 * B i.2)) (mem_univ (i, i)))

Похожие утверждения