Feat/projective with seminorms

Mathlib.lean

@@ -2230,6 +2230,7 @@ public import Mathlib.Analysis.Normed.Module.RieszLemma
 public import Mathlib.Analysis.Normed.Module.Shrink
 public import Mathlib.Analysis.Normed.Module.Span
 public import Mathlib.Analysis.Normed.Module.TransferInstance
+public import Mathlib.Analysis.Normed.Module.TensorProduct.ProjectiveSeminorm
 public import Mathlib.Analysis.Normed.Module.WeakDual
 public import Mathlib.Analysis.Normed.MulAction
 public import Mathlib.Analysis.Normed.Operator.Asymptotics

Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

@@ -263,8 +263,8 @@ theorem fourierIntegral_fderiv [MeasurableSpace V] [BorelSpace V] [FiniteDimensi
   /- First rewrite things in a simplified form, without any real change. -/
   suffices ∫ x, g x • fderiv ℝ f x y ∂μ = ∫ x, (2 * ↑π * I * L y w * g x) • f x ∂μ by
     rw [fourierIntegral_continuousLinearMap_apply' hf']
-    simpa only [fourierIntegral, ContinuousLinearMap.toLinearMap₁₂_apply, fourierSMulRight_apply,
-      neg_apply, ContinuousLinearMap.flip_apply, ← integral_smul, neg_smul,
+    simpa only [fourierIntegral, ContinuousLinearMap.toLinearMap₁₂_apply_apply_apply,
+      fourierSMulRight_apply, neg_apply, ContinuousLinearMap.flip_apply, ← integral_smul, neg_smul,
       smul_neg, ← smul_smul, coe_smul, neg_neg]
   -- Key step: integrate by parts with respect to `y` to switch the derivative from `f` to `g`.
   have A x : fderiv ℝ g x y = - 2 * ↑π * I * L y w * g x :=

Mathlib/Analysis/LocallyConvex/TensorProduct/Projective.lean

@@ -0,0 +1,35 @@
+module
+
+public import Mathlib.Analysis.Normed.Module.TensorProduct.ProjectiveSeminorm
+public import Mathlib.Topology.Algebra.Module.TensorProduct.Projective
+
+import Mathlib.Analysis.Seminorm
+
+@[expose] public section
+
+open TensorProduct Seminorm NNReal WithSeminorms
+
+variable {𝕜 X Y : Type*}
+
+variable [NormedField 𝕜] [PartialOrder 𝕜]
+variable [AddCommGroup X] [Module 𝕜 X] [TopologicalSpace X] [PolynormableSpace 𝕜 X]
+variable [AddCommGroup Y] [Module 𝕜 Y] [TopologicalSpace Y] [PolynormableSpace 𝕜 Y]
+
+variable {ιX ιY : Type*}
+
+variable (p : SeminormFamily 𝕜 X ιX) (q : SeminormFamily 𝕜 Y ιY)
+
+noncomputable def ProjectiveSeminormFamily : SeminormFamily 𝕜 (X ⊗[𝕜]π Y) (ιX × ιY) := fun ⟨i, j⟩ ↦
+  letI := AddGroupSeminorm.toSeminormedAddCommGroup (p i).toAddGroupSeminorm
+  letI := AddGroupSeminorm.toSeminormedAddCommGroup (q j).toAddGroupSeminorm
+  letI : NormedSpace 𝕜 X := ⟨fun a b ↦ ((p i).smul' a b).le⟩
+  letI : NormedSpace 𝕜 Y := ⟨fun a b ↦ ((q j).smul' a b).le⟩
+  projectiveSeminorm
+
+
+
+
+-- /-- The projective tensor topology is strictly induced by the projective seminorm family. -/
+-- theorem withSeminorms_projectiveTensorProduct :
+--     WithSeminorms (ProjectiveSeminormFamily p q) (topology := instTopologicalSpaceProjectiveTensorProduct) := by
+--   sorry

Mathlib/Analysis/Normed/Module/TensorProduct/ProjectiveSeminorm.lean

@@ -0,0 +1,170 @@
+/-
+Copyright (c) 2026 Michał Pacholski. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michał Pacholski
+-/
+
+module
+
+public import Mathlib.Analysis.Normed.Operator.Bilinear
+
+/-!
+# Projective seminorm on the tensor of two normed spaces.
+
+Let `𝕜` be a normed field and `X` and `Y` be normed `𝕜`-vector spaces.
+We define a seminorm on `X ⊗[𝕜] Y`, which we call the "projective seminorm".
+For `t` an element of `X ⊗[𝕜] Y`, its projective seminorm is the
+infimum over all expressions of `t` as `∑ j, xⱼ ⊗ₜ[𝕜] yⱼ` (with the `(xⱼ,yⱼ)` ∈ `X × Y`)
+of `∑ j, ‖xⱼ‖ * ‖yⱼ‖ `.
+
+In particular, every norm `‖.‖` on `X ⨂[𝕜] Y` satisfying `‖x ⊗ₜ[𝕜] y‖ ≤ ‖x‖ * ‖y‖`
+for every `(x,y)` in `X × Y` is bounded above by the projective seminorm.
+
+## Main definitions
+
+* `TensorProduct.projectiveSeminorm`: The projective seminorm on `X ⨂[𝕜] Y`.
+
+## Main results
+
+* `TensorProduct.norm_eval_le_projectiveSeminorm`: If `f` is a continuous bilinear map on
+  `X × Y` and `x` is in `X ⊗[𝕜] Y`, then `‖lift (toLinearMap₁₂ f) x‖ ≤ ‖f‖ * ‖x‖`.
+
+## TODO
+* Port definitions and theorems connected to:
+  *  `PiTensorProduct.liftEquiv`: The bijection between `X →L[𝕜] Y →L[𝕜] F` and
+     `(X ⊗[𝕜] Y) →L[𝕜] F`, as a continuous linear equivalence.
+  *  Port definitions and theorems connected to `PiTensorProduct.liftIsometry`: The bijection
+     between X →L[𝕜] Y →L[𝕜] F` and `(X ⊗[𝕜] Y) →L[𝕜] F`,, as an isometric linear equivalence.
+  *  `PiTensorProduct.tprodL`: The canonical continuous bilinear map from `X × Y`
+     to `X ⊗[𝕜] Y`.
+* Adapt the remaining functoriality constructions/properties from `PiTensorProduct`.
+* If the base field is `ℝ` or `ℂ` (or more generally if the injection of `X` and `Y` into its bidual
+  is an isometry), then we have `projectiveSeminorm x ⊗ₜ[𝕜] y = ‖x‖*‖y‖`.
+* If all `Eᵢ` are separated and satisfy `SeparatingDual`, then the seminorm on
+  `⨂[𝕜] i, Eᵢ` is a norm.
+
+-/
+
+@[expose] public section
+
+variable {𝕜 X Y : Type*}
+variable [SeminormedAddCommGroup X]
+variable [SeminormedAddCommGroup Y]
+
+open scoped TensorProduct
+
+namespace TensorProduct
+
+section NormedField
+
+variable [NormedField 𝕜]
+
+/-- A lift of the projective seminorm to `FreeAddMonoid (X × Y)`, useful to prove the
+properties of `projectiveSeminorm`. -/
+def projectiveSeminormAux : FreeAddMonoid (X × Y) → ℝ :=
+  fun p ↦ (p.toList.map (fun p ↦ ‖p.1‖ * ‖p.2‖)).sum
+
+theorem projectiveSeminormAux_nonneg (p : FreeAddMonoid (X × Y)) :
+    0 ≤ projectiveSeminormAux p := by
+  refine List.sum_nonneg fun a ↦ ?_
+  simp only [List.mem_map, Prod.exists, forall_exists_index, and_imp]
+  intro x y _ rfl
+  positivity
+
+theorem projectiveSeminormAux_add_le (p q : FreeAddMonoid (X × Y)) :
+    projectiveSeminormAux (p + q) ≤ projectiveSeminormAux p + projectiveSeminormAux q := by
+  simp only [projectiveSeminormAux, FreeAddMonoid.toList_add, List.map_append, List.sum_append,
+    Std.le_refl]
+
+variable [NormedSpace 𝕜 X]
+
+theorem projectiveSeminormAux_smul (p : FreeAddMonoid (X × Y)) (a : 𝕜) :
+    projectiveSeminormAux (p.map (fun (y : X × Y) ↦ (a • y.1, y.2))) =
+    ‖a‖ * projectiveSeminormAux p := by
+  simp only [projectiveSeminormAux, FreeAddMonoid.toList_map, List.map_map, Function.comp_def]
+  simp_rw [norm_smul, mul_assoc]
+  rw [List.sum_map_mul_left]
+
+variable [NormedSpace 𝕜 Y]
+
+theorem bddBelow_projectiveSemiNormAux (x : X ⊗[𝕜] Y) :
+    BddBelow (Set.range (fun (p : lifts x) ↦ projectiveSeminormAux p.1)) :=
+  ⟨0, by simp [mem_lowerBounds, projectiveSeminormAux_nonneg]⟩
+
+noncomputable instance : Norm (X ⊗[𝕜] Y) :=
+  ⟨fun x ↦ iInf (fun (p : lifts x) ↦ projectiveSeminormAux p.val)⟩
+
+theorem norm_def (x : X ⊗[𝕜] Y) :
+    ‖x‖ = iInf (fun (p : lifts x) ↦ projectiveSeminormAux p.val) := rfl
+
+theorem projectiveSeminorm_zero : ‖(0 : X ⊗[𝕜] Y)‖ = 0 :=
+  le_antisymm (ciInf_le (bddBelow_projectiveSemiNormAux _) ⟨0, lifts_zero⟩)
+    (le_ciInf (fun p ↦ projectiveSeminormAux_nonneg p.val))
+
+theorem projectiveSeminorm_add_le (x y : X ⊗[𝕜] Y) : ‖x + y‖ ≤ ‖x‖ + ‖y‖ :=
+  le_ciInf_add_ciInf (fun p q ↦ ciInf_le_of_le (bddBelow_projectiveSemiNormAux _)
+    ⟨p.1 + q.1, lifts_add p.2 q.2⟩ (projectiveSeminormAux_add_le p.1 q.1))
+
+theorem projectiveSeminorm_smul_le (a : 𝕜) (x : X ⊗[𝕜] Y) : ‖a • x‖ ≤ ‖a‖ * ‖x‖ := by
+  simp only [norm_def, Real.mul_iInf_of_nonneg (norm_nonneg _)]
+  refine le_ciInf fun p ↦ ?_
+  simpa [projectiveSeminormAux_smul] using
+    ciInf_le_of_le (bddBelow_projectiveSemiNormAux _) ⟨_, lifts_smul p.2 a⟩ (le_refl _)
+
+/-- The projective seminorm on `X ⊗[𝕜] Y`. It sends an element `x` of `X ⊗[𝕜] Y` to the
+infimum over all expressions of `x` as `∑ j, xⱼ ⊗ₜ[𝕜] yⱼ` (with the `(xⱼ,yⱼ)` ∈ `X × Y`)
+of `∑ j, ‖xⱼ‖ * ‖yⱼ‖ `. -/
+noncomputable def projectiveSeminorm : Seminorm 𝕜 (X ⊗[𝕜] Y) := .ofSMulLE
+    _ projectiveSeminorm_zero projectiveSeminorm_add_le projectiveSeminorm_smul_le
+
+noncomputable instance : SeminormedAddCommGroup (X ⊗[𝕜] Y) :=
+  fast_instance% AddGroupSeminorm.toSeminormedAddCommGroup projectiveSeminorm.toAddGroupSeminorm
+
+noncomputable instance : NormedSpace 𝕜 (X ⊗[𝕜] Y) := ⟨projectiveSeminorm_smul_le⟩
+
+theorem projectiveSeminorm_tprod_le (x : X) (y : Y) :
+    projectiveSeminorm (x ⊗ₜ[𝕜] y) ≤ ‖x‖*‖y‖ := by
+  convert! ciInf_le (bddBelow_projectiveSemiNormAux _) ⟨FreeAddMonoid.of (x, y), ?_⟩
+  · simp [projectiveSeminormAux]
+  · simp [mem_lifts_iff]
+
+end NormedField
+
+section NontriviallyNormedField
+
+variable [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 X] [NormedSpace 𝕜 Y]
+
+open ContinuousLinearMap
+
+example {G : Type*} [SeminormedAddCommGroup G]
+    [NormedSpace 𝕜 G] (f : X →L[𝕜] Y →L[𝕜] G) : X →ₗ[𝕜] Y →ₗ[𝕜] G :=
+  (coeLM 𝕜 ∘ₗ f.toLinearMap)
+
+theorem norm_eval_le_projectiveSeminorm {G : Type*} [SeminormedAddCommGroup G]
+    [NormedSpace 𝕜 G] (f : X →L[𝕜] Y →L[𝕜] G) (x : X ⊗[𝕜] Y) :
+    ‖lift (toLinearMap₁₂ f) x‖ ≤ ‖f‖ * ‖x‖ := by
+  rw [norm_def, mul_comm, Real.iInf_mul_of_nonneg (norm_nonneg _)]
+  refine le_ciInf fun ⟨p, hp⟩ ↦ ?_
+  rw! [← ((mem_lifts_iff x p).mp hp), ← List.sum_map_hom, ← Multiset.sum_coe]
+  grw [norm_multiset_sum_le]
+  simp only [mul_comm, ← smul_eq_mul, List.smul_sum, projectiveSeminormAux]
+  refine List.Forall₂.sum_le_sum ?_
+  simpa [←mul_assoc, mul_comm] using fun x y _ ↦
+    ((f x).le_opNorm y).trans (mul_le_mul_of_nonneg_right (f.le_opNorm x) (norm_nonneg y))
+
+lemma _root_.ContinuousLinearMap.le_opNorm_tprod {𝕜 X Y F : Type*}
+    [NontriviallyNormedField 𝕜]
+    [SeminormedAddCommGroup X] [NormedSpace 𝕜 X]
+    [SeminormedAddCommGroup Y] [NormedSpace 𝕜 Y]
+    [SeminormedAddCommGroup F] [NormedSpace 𝕜 F]
+    (l : X ⊗[𝕜] Y →L[𝕜] F) (x : X) (y : Y) :
+    ‖l (x ⊗ₜ[𝕜] y)‖ ≤ ‖l‖ * ‖x‖ * ‖y‖ := by
+    calc
+      ‖l (x ⊗ₜ[𝕜] y)‖ ≤ ‖l‖ * projectiveSeminorm (x ⊗ₜ[𝕜] y) := l.le_opNorm (x ⊗ₜ[𝕜] y)
+      _ ≤ ‖l‖ * (‖x‖ * ‖y‖) := mul_le_mul_of_nonneg_left (projectiveSeminorm_tprod_le x y)
+        (norm_nonneg l)
+      _ = ‖l‖ * ‖x‖ * ‖y‖ := by rw [mul_assoc]
+
+end NontriviallyNormedField
+
+end TensorProduct

Mathlib/LinearAlgebra/TensorProduct/Basic.lean

@@ -82,6 +82,62 @@ theorem liftAddHom_tmul (f : M →+ N →+ P)
     liftAddHom f hf (m ⊗ₜ n) = f m n :=
   rfl
 
+/-- The image of an element `p` of `FreeAddMonoid (M × N)` in the `TensorProduct` is
+equal to the sum of `x ⊗ₜ y` over all the entries `(x, y)` of `p`.
+-/
+lemma _root_.FreeAddMonoid.toTensorProduct (p : FreeAddMonoid (M × N)) :
+    AddCon.toQuotient (c := addConGen (TensorProduct.Eqv R M N)) p =
+    (p.toList.map (fun x ↦ x.1 ⊗ₜ[R] x.2)).sum := by
+  induction p using FreeAddMonoid.inductionOn' with
+  | zero => rfl
+  | add_of b a ih =>
+    rw [FreeAddMonoid.toList_of_add, List.map_cons, List.sum_cons, ← ih]
+    rfl
+
+/-- The set of lifts of an element `x` of `M ⊗[R] N` in `FreeAddMonoid (M × N)`. -/
+def lifts (x : M ⊗[R] N) : Set (FreeAddMonoid (M × N)) :=
+  {p | AddCon.toQuotient (c := addConGen (TensorProduct.Eqv R M N)) p = x}
+
+lemma mem_lifts_iff (x : M ⊗[R] N) (p : FreeAddMonoid (M × N)) :
+    p ∈ lifts x ↔ List.sum (List.map (fun x ↦ x.1 ⊗ₜ[R] x.2) p.toList) = x := by
+  simp only [lifts, Set.mem_ofPred_eq, FreeAddMonoid.toTensorProduct]
+  rfl
+
+/-- Every element of `M ⊗[R] N` has a lift in `FreeAddMonoid (M × N)`.
+-/
+lemma nonempty_lifts (x : M ⊗[R] N) : Set.Nonempty (lifts x) := by
+  existsi Quot.out x
+  exact Function.surjInv_eq Quot.exists_rep x
+
+instance (x : M ⊗[R] N) : Nonempty ↑x.lifts := nonempty_subtype.mpr (nonempty_lifts x)
+
+/-- The empty list lifts the element `0` of `M ⊗[R] N`.
+-/
+lemma lifts_zero : 0 ∈ lifts (0 : M ⊗[R] N) := by
+  rw [mem_lifts_iff, FreeAddMonoid.toList_zero, List.map_nil, List.sum_nil]
+
+set_option backward.isDefEq.respectTransparency false in
+/-- If elements `p, q` of `FreeAddMonoid (M × N)` lift elements `x, y` of `M ⊗[R] N`
+respectively, then `p + q` lifts `x + y`.
+-/
+lemma lifts_add {x y : M ⊗[R] N} {p q : FreeAddMonoid (M × N)}
+    (hp : p ∈ lifts x) (hq : q ∈ lifts y) : p + q ∈ lifts (x + y) := by
+  simp only [lifts, Set.mem_ofPred_eq, AddCon.coe_add]
+  rw [hp, hq]
+
+/-- If an element `p` of `FreeAddMonoid (M × N)` lifts an element `x` of `M ⊗[R] N`,
+and if `a` is an element of `R`, then the list obtained by multiplying the first entry of each
+element of `p` by `a` lifts `a • x`.
+-/
+lemma lifts_smul {x : M ⊗[R] N} {p : FreeAddMonoid (M × N)} (h : p ∈ lifts x) (a : R) :
+    p.map (fun (y : M × N) ↦ (a • y.1, y.2)) ∈ lifts (a • x) := by
+  rw [mem_lifts_iff] at h ⊢
+  rw [← h]
+  simp only [FreeAddMonoid.toList_map, List.map_map]
+  induction p.toList with
+  | nil => simp
+  | cons hd tl ih => simp [ih, smul_add, smul_tmul]
+
 end Module
 
 variable [Module R P] [Module R Q]

Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean

@@ -66,7 +66,6 @@ lemma continuous_charFun : Continuous (charFun μ) := by
   refine contDiff_zero.1 (contDiff_charFun ?_)
   simpa using by fun_prop
 
-set_option backward.isDefEq.respectTransparency false in
 theorem iteratedFDeriv_charFun {n : ℕ} {t : E} (hint : MemLp id n μ) (x : Fin n → E) :
     iteratedFDeriv ℝ n (charFun μ) t x = I ^ n * ∫ y, (∏ i, ⟪y, x i⟫) * exp (⟪y, t⟫ * I) ∂μ := by
   have h : innerₗ E = (innerSL ℝ).toLinearMap₁₂ := rfl
@@ -85,8 +84,8 @@ theorem iteratedFDeriv_charFun {n : ℕ} {t : E} (hint : MemLp id n μ) (x : Fin
   rw [fourierIntegral_continuousMultilinearMap_apply Real.continuous_fourierChar]
   swap;
   · exact integrable_fourierPowSMulRight _ (by simpa using hint.integrable_norm_pow') (by fun_prop)
-  simp only [fourierIntegral, Real.fourierChar, Circle.exp, ContinuousMap.coe_mk, ofReal_mul,
-    ofReal_ofNat, innerSL, map_neg, map_smul, ContinuousLinearMap.toLinearMap₁₂_apply,
+  simp only [fourierIntegral, Real.fourierChar, Circle.coe_exp, ofReal_mul,
+    ofReal_ofNat, innerSL, map_neg, map_smul, ContinuousLinearMap.toLinearMap₁₂_apply_apply_apply,
     LinearMap.mkContinuous₂_apply, innerₛₗ_apply_apply, smul_eq_mul, neg_neg, AddChar.coe_mk,
     ofReal_inv, fourierPowSMulRight_apply, Pi.ofNat_apply, real_smul, ofReal_prod, mul_one,
     Circle.smul_def]

Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean

@@ -299,14 +299,17 @@ theorem map_smulₛₗ₂ (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (c : R) (x
     f (c • x) y = σ₁₃ c • f x y := by rw [f.map_smulₛₗ, smul_apply]
 
 /-- Send a continuous sesquilinear map to an abstract sesquilinear map (forgetting continuity). -/
-def toLinearMap₁₂ (L : E →SL[σ₁₃] F →SL[σ₂₃] G) : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G :=
-  (coeLMₛₗ σ₂₃).comp L.toLinearMap
+@[simps -isSimp apply]
+def toLinearMap₁₂ : (E →SL[σ₁₃] F →SL[σ₂₃] G) →ₗ[𝕜₃] E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G where
+  toFun L := (coeLMₛₗ σ₂₃).comp L.toLinearMap
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
 
-@[simp] lemma toLinearMap₁₂_apply (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) :
+@[simp] lemma toLinearMap₁₂_apply_apply_apply (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) :
     L.toLinearMap₁₂ v w = L v w := rfl
 
 lemma toLinearMap₁₂_injective :
-    (toLinearMap₁₂ (E := E) (F := F) (G := G) (σ₁₃ := σ₁₃) (σ₂₃ := σ₂₃)).Injective := by
+    (toLinearMap₁₂ (E := E) (F := F) (G := G) (σ₁₃ := σ₁₃) (σ₂₃ := σ₂₃) : _ → _).Injective := by
   simp [Function.Injective, LinearMap.ext_iff, ← ContinuousLinearMap.ext_iff]
 
 lemma toLinearMap₁₂_inj (L₁ L₂ : E →SL[σ₁₃] F →SL[σ₂₃] G) :