From b31173ee05c911d61ad6a05bd2196835c932e0ec Mon Sep 17 00:00:00 2001
From: Moritz Doll <moritz.doll@googlemail.com>
Date: Tue, 28 Mar 2023 01:31:58 +0000
Subject: [PATCH] chore(analysis/locally_convex/with_seminorms): remove
 unnecessary positivity assumption (#18659)

In the boundedness definition it is not necessary to assume that the bound is positive.
---
 .../locally_convex/with_seminorms.lean        | 40 +++++++++----------
 src/analysis/schwartz_space.lean              |  4 +-
 2 files changed, 21 insertions(+), 23 deletions(-)

diff --git a/src/analysis/locally_convex/with_seminorms.lean b/src/analysis/locally_convex/with_seminorms.lean
index a39d6f380a131..a578827117d1d 100644
--- a/src/analysis/locally_convex/with_seminorms.lean
+++ b/src/analysis/locally_convex/with_seminorms.lean
@@ -221,46 +221,42 @@ variables {σ₁₂ : 𝕜 →+* 𝕜₂} [ring_hom_isometric σ₁₂]
 
 /-- The proposition that a linear map is bounded between spaces with families of seminorms. -/
 def is_bounded (p : ι → seminorm 𝕜 E) (q : ι' → seminorm 𝕜₂ F) (f : E →ₛₗ[σ₁₂] F) : Prop :=
-  ∀ i, ∃ s : finset ι, ∃ C : ℝ≥0, C ≠ 0 ∧ (q i).comp f ≤ C • s.sup p
+  ∀ i, ∃ s : finset ι, ∃ C : ℝ≥0, (q i).comp f ≤ C • s.sup p
 
 lemma is_bounded_const (ι' : Type*) [nonempty ι']
   {p : ι → seminorm 𝕜 E} {q : seminorm 𝕜₂ F} (f : E →ₛₗ[σ₁₂] F) :
-  is_bounded p (λ _ : ι', q) f ↔ ∃ (s : finset ι) C : ℝ≥0, C ≠ 0 ∧ q.comp f ≤ C • s.sup p :=
+  is_bounded p (λ _ : ι', q) f ↔ ∃ (s : finset ι) C : ℝ≥0, q.comp f ≤ C • s.sup p :=
 by simp only [is_bounded, forall_const]
 
 lemma const_is_bounded (ι : Type*) [nonempty ι]
   {p : seminorm 𝕜 E} {q : ι' → seminorm 𝕜₂ F} (f : E →ₛₗ[σ₁₂] F) :
-  is_bounded (λ _ : ι, p) q f ↔ ∀ i, ∃ C : ℝ≥0, C ≠ 0 ∧ (q i).comp f ≤ C • p :=
+  is_bounded (λ _ : ι, p) q f ↔ ∀ i, ∃ C : ℝ≥0, (q i).comp f ≤ C • p :=
 begin
   split; intros h i,
-  { rcases h i with ⟨s, C, hC, h⟩,
-    exact ⟨C, hC, le_trans h (smul_le_smul (finset.sup_le (λ _ _, le_rfl)) le_rfl)⟩ },
+  { rcases h i with ⟨s, C, h⟩,
+    exact ⟨C, le_trans h (smul_le_smul (finset.sup_le (λ _ _, le_rfl)) le_rfl)⟩ },
   use [{classical.arbitrary ι}],
   simp only [h, finset.sup_singleton],
 end
 
 lemma is_bounded_sup {p : ι → seminorm 𝕜 E} {q : ι' → seminorm 𝕜₂ F}
   {f : E →ₛₗ[σ₁₂] F} (hf : is_bounded p q f) (s' : finset ι') :
-  ∃ (C : ℝ≥0) (s : finset ι), 0 < C ∧ (s'.sup q).comp f ≤ C • (s.sup p) :=
+  ∃ (C : ℝ≥0) (s : finset ι), (s'.sup q).comp f ≤ C • (s.sup p) :=
 begin
   classical,
   obtain rfl | hs' := s'.eq_empty_or_nonempty,
-  { exact ⟨1, ∅, zero_lt_one, by simp [seminorm.bot_eq_zero]⟩ },
+  { exact ⟨1, ∅, by simp [seminorm.bot_eq_zero]⟩ },
   choose fₛ fC hf using hf,
   use [s'.card • s'.sup fC, finset.bUnion s' fₛ],
-  split,
-  { refine nsmul_pos _ (ne_of_gt (finset.nonempty.card_pos hs')),
-    cases finset.nonempty.bex hs' with j hj,
-    exact lt_of_lt_of_le (zero_lt_iff.mpr (and.elim_left (hf j))) (finset.le_sup hj) },
   have hs : ∀ i : ι', i ∈ s' → (q i).comp f ≤ s'.sup fC • ((finset.bUnion s' fₛ).sup p) :=
   begin
     intros i hi,
-    refine le_trans (and.elim_right (hf i)) (smul_le_smul _ (finset.le_sup hi)),
+    refine (hf i).trans (smul_le_smul _ (finset.le_sup hi)),
     exact finset.sup_mono (finset.subset_bUnion_of_mem fₛ hi),
   end,
-  refine le_trans (comp_mono f (finset_sup_le_sum q s')) _,
+  refine (comp_mono f (finset_sup_le_sum q s')).trans _,
   simp_rw [←pullback_apply, add_monoid_hom.map_sum, pullback_apply],
-  refine le_trans (finset.sum_le_sum hs) _,
+  refine (finset.sum_le_sum hs).trans _,
   rw [finset.sum_const, smul_assoc],
   exact le_rfl,
 end
@@ -608,20 +604,22 @@ begin
   refine continuous_of_continuous_comp hq _ (λ i, seminorm.continuous_of_continuous_at_zero _),
   rw [metric.continuous_at_iff', map_zero],
   intros r hr,
-  rcases hf i with ⟨s₁, C, hC, hf⟩,
-  have hC' : 0 < C := hC.bot_lt,
+  rcases hf i with ⟨s₁, C, hf⟩,
+  have hC' : 0 < C + 1 := by positivity,
   rw hp.has_basis.eventually_iff,
-  refine ⟨(s₁.sup p).ball 0 (r/C), p.basis_sets_mem _ (by positivity), _⟩,
+  refine ⟨(s₁.sup p).ball 0 (r/(C + 1)), p.basis_sets_mem _ (by positivity), _⟩,
   simp_rw [ ←metric.mem_ball, ←mem_preimage, ←ball_zero_eq_preimage_ball],
   refine subset.trans _ (ball_antitone hf),
-  rw ball_smul (s₁.sup p) hC',
-  refl
+  norm_cast,
+  rw ← ball_smul (s₁.sup p) hC',
+  refine ball_antitone (smul_le_smul le_rfl _),
+  simp only [le_add_iff_nonneg_right, zero_le'],
 end
 
 lemma cont_with_seminorms_normed_space (F) [seminormed_add_comm_group F] [normed_space 𝕝₂ F]
   [uniform_space E] [uniform_add_group E]
   {p : ι → seminorm 𝕝 E} (hp : with_seminorms p) (f : E →ₛₗ[τ₁₂] F)
-  (hf : ∃ (s : finset ι) C : ℝ≥0, C ≠ 0 ∧ (norm_seminorm 𝕝₂ F).comp f ≤ C • s.sup p) :
+  (hf : ∃ (s : finset ι) C : ℝ≥0, (norm_seminorm 𝕝₂ F).comp f ≤ C • s.sup p) :
   continuous f :=
 begin
   rw ←seminorm.is_bounded_const (fin 1) at hf,
@@ -631,7 +629,7 @@ end
 lemma cont_normed_space_to_with_seminorms (E) [seminormed_add_comm_group E] [normed_space 𝕝 E]
   [uniform_space F] [uniform_add_group F]
   {q : ι → seminorm 𝕝₂ F} (hq : with_seminorms q) (f : E →ₛₗ[τ₁₂] F)
-  (hf : ∀ i : ι, ∃ C : ℝ≥0, C ≠ 0 ∧ (q i).comp f ≤ C • (norm_seminorm 𝕝 E)) : continuous f :=
+  (hf : ∀ i : ι, ∃ C : ℝ≥0, (q i).comp f ≤ C • (norm_seminorm 𝕝 E)) : continuous f :=
 begin
   rw ←seminorm.const_is_bounded (fin 1) at hf,
   exact continuous_from_bounded (norm_with_seminorms 𝕝 E) hq f hf,
diff --git a/src/analysis/schwartz_space.lean b/src/analysis/schwartz_space.lean
index a29de8178f72d..0a2d35e132e9a 100644
--- a/src/analysis/schwartz_space.lean
+++ b/src/analysis/schwartz_space.lean
@@ -504,7 +504,7 @@ def fderiv_clm : 𝓢(E, F) →L[𝕜] 𝓢(E, E →L[ℝ] F) :=
     refine seminorm.continuous_from_bounded (schwartz_with_seminorms 𝕜 E F)
       (schwartz_with_seminorms 𝕜 E (E →L[ℝ] F)) _ _,
     rintros ⟨k, n⟩,
-    use [{⟨k, n+1⟩}, 1, one_ne_zero],
+    use [{⟨k, n+1⟩}, 1],
     intros f,
     simp only [schwartz_seminorm_family_apply, seminorm.comp_apply, finset.sup_singleton, one_smul],
     refine (fderiv_lm 𝕜 f).seminorm_le_bound 𝕜 k n (by positivity) _,
@@ -556,7 +556,7 @@ def to_bounded_continuous_function_clm : 𝓢(E, F) →L[𝕜] E →ᵇ F :=
   begin
     change continuous (to_bounded_continuous_function_lm 𝕜 E F),
     refine seminorm.continuous_from_bounded (schwartz_with_seminorms 𝕜 E F)
-      (norm_with_seminorms 𝕜 (E →ᵇ F)) _ (λ i, ⟨{0}, 1, one_ne_zero, λ f, _⟩),
+      (norm_with_seminorms 𝕜 (E →ᵇ F)) _ (λ i, ⟨{0}, 1, λ f, _⟩),
     rw [finset.sup_singleton, one_smul , seminorm.comp_apply, coe_norm_seminorm,
         schwartz_seminorm_family_apply_zero, bounded_continuous_function.norm_le (map_nonneg _ _)],
     intros x,