chore: make CLM.extend total and define LM.leftInverse (#31799)

- Make `ContinuousLinearMap.extend` a total function
- Define `LinearMap.leftInverse` as a total function with junk value if the input is not invertible.

Required for #31074

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: mcdoll

Mathlib/Analysis/InnerProductSpace/LinearPMap.lean

@@ -106,39 +106,40 @@ theorem adjointDomainMkCLM_apply (y : T.adjointDomain) (x : T.domain) :
     adjointDomainMkCLM T y x = ⟪(y : F), T x⟫ :=
   rfl
 
-variable {T}
-variable (hT : Dense (T.domain : Set E))
-
 /-- The unique continuous extension of the operator `adjointDomainMkCLM` to `E`. -/
 def adjointDomainMkCLMExtend (y : T.adjointDomain) : StrongDual 𝕜 E :=
-  (T.adjointDomainMkCLM y).extend (Submodule.subtypeL T.domain) hT.denseRange_val
-    isUniformEmbedding_subtype_val.isUniformInducing
+  (T.adjointDomainMkCLM y).extend (Submodule.subtypeL T.domain)
+
+variable {T}
 
 @[simp]
-theorem adjointDomainMkCLMExtend_apply (y : T.adjointDomain) (x : T.domain) :
-    adjointDomainMkCLMExtend hT y (x : E) = ⟪(y : F), T x⟫ :=
-  ContinuousLinearMap.extend_eq _ _ _ _ _
+theorem adjointDomainMkCLMExtend_apply (hT : Dense (T.domain : Set E)) (y : T.adjointDomain)
+    (x : T.domain) : adjointDomainMkCLMExtend T y (x : E) = ⟪(y : F), T x⟫ :=
+  ContinuousLinearMap.extend_eq _ hT.denseRange_val
+    isUniformEmbedding_subtype_val.isUniformInducing _
 
 variable [CompleteSpace E]
 
+variable (hT : Dense (T.domain : Set E))
+
 /-- The adjoint as a linear map from its domain to `E`.
 
 This is an auxiliary definition needed to define the adjoint operator as a `LinearPMap` without
 the assumption that `T.domain` is dense. -/
 def adjointAux : T.adjointDomain →ₗ[𝕜] E where
-  toFun y := (InnerProductSpace.toDual 𝕜 E).symm (adjointDomainMkCLMExtend hT y)
+  toFun y := (InnerProductSpace.toDual 𝕜 E).symm (adjointDomainMkCLMExtend T y)
   map_add' x y :=
     hT.eq_of_inner_left fun _ => by
       simp only [inner_add_left, Submodule.coe_add, InnerProductSpace.toDual_symm_apply,
-        adjointDomainMkCLMExtend_apply]
+        adjointDomainMkCLMExtend_apply hT]
   map_smul' _ _ :=
     hT.eq_of_inner_left fun _ => by
       simp only [inner_smul_left, Submodule.coe_smul_of_tower, RingHom.id_apply,
-        InnerProductSpace.toDual_symm_apply, adjointDomainMkCLMExtend_apply]
+        InnerProductSpace.toDual_symm_apply, adjointDomainMkCLMExtend_apply hT]
 
 theorem adjointAux_inner (y : T.adjointDomain) (x : T.domain) :
     ⟪adjointAux hT y, x⟫ = ⟪(y : F), T x⟫ := by
-  simp [adjointAux]
+  simp [adjointAux, hT]
 
 theorem adjointAux_unique (y : T.adjointDomain) {x₀ : E}
     (hx₀ : ∀ x : T.domain, ⟪x₀, x⟫ = ⟪(y : F), T x⟫) : adjointAux hT y = x₀ :=

Mathlib/Analysis/Normed/Operator/Extend.lean

@@ -41,44 +41,52 @@ variable [AddCommGroup E] [UniformSpace E] [IsUniformAddGroup E]
   [ContinuousConstSMul 𝕜 Eₗ] [ContinuousConstSMul 𝕜₂ F]
   {σ₁₂ : 𝕜 →+* 𝕜₂} (f g : E →SL[σ₁₂] F) [CompleteSpace F] (e : E →L[𝕜] Eₗ)
 
-variable (h_dense : DenseRange e) (h_e : IsUniformInducing e)
-
+open scoped Classical in
 /-- Extension of a continuous linear map `f : E →SL[σ₁₂] F`, with `E` a normed space and `F` a
 complete normed space, along a uniform and dense embedding `e : E →L[𝕜] Eₗ`. -/
 def extend : Eₗ →SL[σ₁₂] F :=
+  if h : DenseRange e ∧ IsUniformInducing e then
   -- extension of `f` is continuous
-  have cont := (uniformContinuous_uniformly_extend h_e h_dense f.uniformContinuous).continuous
+  have cont := (uniformContinuous_uniformly_extend h.2 h.1 f.uniformContinuous).continuous
   -- extension of `f` agrees with `f` on the domain of the embedding `e`
-  have eq := uniformly_extend_of_ind h_e h_dense f.uniformContinuous
-  { toFun := (h_e.isDenseInducing h_dense).extend f
+  have eq := uniformly_extend_of_ind h.2 h.1 f.uniformContinuous
+  { toFun := (h.2.isDenseInducing h.1).extend f
     map_add' := by
-      refine h_dense.induction_on₂ ?_ ?_
+      refine h.1.induction_on₂ ?_ ?_
       · exact isClosed_eq (cont.comp continuous_add)
           ((cont.comp continuous_fst).add (cont.comp continuous_snd))
       · intro x y
         simp only [eq, ← e.map_add]
         exact f.map_add _ _
     map_smul' := fun k => by
-      refine fun b => h_dense.induction_on b ?_ ?_
+      refine fun b => h.1.induction_on b ?_ ?_
       · exact isClosed_eq (cont.comp (continuous_const_smul _))
           ((continuous_const_smul _).comp cont)
       · intro x
         rw [← map_smul]
         simp only [eq]
         exact ContinuousLinearMap.map_smulₛₗ _ _ _
     cont }
+  else 0
 
-@[simp]
-theorem extend_eq (x : E) : extend f e h_dense h_e (e x) = f x :=
-  IsDenseInducing.extend_eq (h_e.isDenseInducing h_dense) f.cont _
+variable {e}
 
-theorem extend_unique (g : Eₗ →SL[σ₁₂] F) (H : g.comp e = f) : extend f e h_dense h_e = g :=
-  ContinuousLinearMap.coeFn_injective <|
+@[simp]
+theorem extend_eq (h_dense : DenseRange e) (h_e : IsUniformInducing e) (x : E) :
+    extend f e (e x) = f x := by
+  simp only [extend, h_dense, h_e, and_self, ↓reduceDIte, coe_mk', LinearMap.coe_mk, AddHom.coe_mk]
+  exact IsDenseInducing.extend_eq (h_e.isDenseInducing h_dense) f.cont _
+
+theorem extend_unique (h_dense : DenseRange e) (h_e : IsUniformInducing e) (g : Eₗ →SL[σ₁₂] F)
+    (H : g.comp e = f) : extend f e = g := by
+  simp only [extend, h_dense, h_e, and_self, ↓reduceDIte]
+  exact ContinuousLinearMap.coeFn_injective <|
     uniformly_extend_unique h_e h_dense (ContinuousLinearMap.ext_iff.1 H) g.continuous
 
 @[simp]
-theorem extend_zero : extend (0 : E →SL[σ₁₂] F) e h_dense h_e = 0 :=
-  extend_unique _ _ _ _ _ (zero_comp _)
+theorem extend_zero (h_dense : DenseRange e) (h_e : IsUniformInducing e) :
+    extend (0 : E →SL[σ₁₂] F) e = 0 :=
+  extend_unique _ h_dense h_e  _ (zero_comp _)
 
 end Ring
 
@@ -87,16 +95,16 @@ section NormedField
 variable [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂}
   [NormedAddCommGroup E] [NormedAddCommGroup Eₗ] [NormedAddCommGroup F] [NormedAddCommGroup Fₗ]
   [NormedSpace 𝕜 E] [NormedSpace 𝕜 Eₗ] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₂ Fₗ] [CompleteSpace F]
-  (f g : E →SL[σ₁₂] F) (e : E →L[𝕜] Eₗ)
+  (f g : E →SL[σ₁₂] F) {e : E →L[𝕜] Eₗ}
 
 variable (h_dense : DenseRange e) (h_e : IsUniformInducing e)
 
-variable {N : ℝ≥0} (h_e : ∀ x, ‖x‖ ≤ N * ‖e x‖) [RingHomIsometric σ₁₂]
+variable {N : ℝ≥0} [RingHomIsometric σ₁₂]
 
 /-- If a dense embedding `e : E →L[𝕜] G` expands the norm by a constant factor `N⁻¹`, then the
 norm of the extension of `f` along `e` is bounded by `N * ‖f‖`. -/
-theorem opNorm_extend_le :
-    ‖f.extend e h_dense (isUniformEmbedding_of_bound _ h_e).isUniformInducing‖ ≤ N * ‖f‖ := by
+theorem opNorm_extend_le (h_dense : DenseRange e) (h_e : ∀ x, ‖x‖ ≤ N * ‖e x‖) :
+    ‖f.extend e‖ ≤ N * ‖f‖ := by
   -- Add `opNorm_le_of_dense`?
   refine opNorm_le_bound _ ?_ (isClosed_property h_dense (isClosed_le ?_ ?_) fun x ↦ ?_)
   · cases le_total 0 N with
@@ -108,7 +116,7 @@ theorem opNorm_extend_le :
       simp
   · exact (cont _).norm
   · exact continuous_const.mul continuous_norm
-  · rw [extend_eq]
+  · rw [extend_eq _ h_dense (isUniformEmbedding_of_bound _ h_e).isUniformInducing]
     calc
       ‖f x‖ ≤ ‖f‖ * ‖x‖ := le_opNorm _ _
       _ ≤ ‖f‖ * (N * ‖e x‖) := mul_le_mul_of_nonneg_left (h_e x) (norm_nonneg _)

Mathlib/LinearAlgebra/Basis/VectorSpace.lean

@@ -256,9 +256,28 @@ theorem LinearMap.exists_leftInverse_of_injective (f : V →ₗ[K] V') (hf_inj :
   rw [Basis.ofVectorSpace_apply_self, fb_eq, hC.constr_basis]
   exact leftInverse_invFun (LinearMap.ker_eq_bot.1 hf_inj) _
 
+open scoped Classical in
+/-- The left inverse of `f : E →ₗ[𝕜] F`.
+
+If `f` is not injective, then we use the junk value `0`. -/
+noncomputable
+def LinearMap.leftInverse (f : V →ₗ[K] V') : V' →ₗ[K] V :=
+  if h_inj : LinearMap.ker f = ⊥ then
+  (f.exists_leftInverse_of_injective h_inj).choose
+  else 0
+
+theorem LinearMap.leftInverse_comp_of_inj {f : V →ₗ[K] V'} (h_inj : LinearMap.ker f = ⊥) :
+    f.leftInverse ∘ₗ f = LinearMap.id := by
+  simpa [leftInverse, h_inj] using (f.exists_leftInverse_of_injective h_inj).choose_spec
+
+/-- If `f` is injective, then the left inverse composed with `f` is the identity. -/
+theorem LinearMap.leftInverse_apply_of_inj {f : V →ₗ[K] V'} (h_inj : LinearMap.ker f = ⊥) (x : V) :
+    f.leftInverse (f x) = x :=
+  LinearMap.ext_iff.mp (f.leftInverse_comp_of_inj h_inj) x
+
 theorem Submodule.exists_isCompl (p : Submodule K V) : ∃ q : Submodule K V, IsCompl p q :=
-  let ⟨f, hf⟩ := p.subtype.exists_leftInverse_of_injective p.ker_subtype
-  ⟨LinearMap.ker f, LinearMap.isCompl_of_proj <| LinearMap.ext_iff.1 hf⟩
+  ⟨LinearMap.ker p.subtype.leftInverse,
+    LinearMap.isCompl_of_proj <| LinearMap.leftInverse_apply_of_inj p.ker_subtype⟩
 
 instance Submodule.complementedLattice : ComplementedLattice (Submodule K V) :=
   ⟨Submodule.exists_isCompl⟩

Mathlib/LinearAlgebra/Dual/Lemmas.lean

@@ -422,14 +422,13 @@ theorem dualAnnihilator_inj {W W' : Subspace K V} :
 an arbitrary extension of `φ` to an element of the dual of `V`.
 That is, `dualLift W φ` sends `w ∈ W` to `φ x` and `x` in a chosen complement of `W` to `0`. -/
 noncomputable def dualLift (W : Subspace K V) : Module.Dual K W →ₗ[K] Module.Dual K V :=
-  (Classical.choose <| W.subtype.exists_leftInverse_of_injective W.ker_subtype).dualMap
+  W.subtype.leftInverse.dualMap
 
 variable {W : Subspace K V}
 
 @[simp]
 theorem dualLift_of_subtype {φ : Module.Dual K W} (w : W) : W.dualLift φ (w : V) = φ w :=
-  congr_arg φ <| DFunLike.congr_fun
-    (Classical.choose_spec <| W.subtype.exists_leftInverse_of_injective W.ker_subtype) w
+  congr_arg φ <| LinearMap.leftInverse_apply_of_inj W.ker_subtype _
 
 theorem dualLift_of_mem {φ : Module.Dual K W} {w : V} (hw : w ∈ W) : W.dualLift φ w = φ ⟨w, hw⟩ :=
   dualLift_of_subtype ⟨w, hw⟩

Mathlib/MeasureTheory/Function/Holder.lean

@@ -133,9 +133,8 @@ def lpPairing (B : E →L[𝕜] F →L[𝕜] G) : Lp E p μ →L[𝕜] Lp F q μ
 
 lemma lpPairing_eq_integral (f : Lp E p μ) (g : Lp F q μ) :
     B.lpPairing μ p q f g = ∫ x, B (f x) (g x) ∂μ := by
-  change L1.integralCLM _ = _
-  rw [← L1.integral_def, L1.integral_eq_integral]
-  exact integral_congr_ae <| B.coeFn_holder _ _
+  simpa [lpPairing, ← L1.integral_eq', L1.integral_eq_integral] using
+    integral_congr_ae <| B.coeFn_holder _ _
 
 end ContinuousLinearMap
 

Mathlib/MeasureTheory/Integral/Bochner/L1.lean

@@ -530,8 +530,7 @@ open ContinuousLinearMap
 variable (𝕜) in
 /-- The Bochner integral in L1 space as a continuous linear map. -/
 nonrec def integralCLM' : (α →₁[μ] E) →L[𝕜] E :=
-  (integralCLM' α E 𝕜 μ).extend (coeToLp α E 𝕜) (simpleFunc.denseRange one_ne_top)
-    simpleFunc.isUniformInducing
+  (integralCLM' α E 𝕜 μ).extend (coeToLp α E 𝕜)
 
 /-- The Bochner integral in L1 space as a continuous linear map over ℝ. -/
 def integralCLM : (α →₁[μ] E) →L[ℝ] E :=
@@ -554,6 +553,21 @@ theorem SimpleFunc.integral_L1_eq_integral (f : α →₁ₛ[μ] E) :
   simp only [integral, L1.integral]
   exact setToL1_eq_setToL1SCLM (dominatedFinMeasAdditive_weightedSMul μ) f
 
+@[norm_cast]
+theorem SimpleFunc.integralCLM'_L1_eq_integral (f : α →₁ₛ[μ] E) :
+    L1.integralCLM' 𝕜 (f : α →₁[μ] E) = SimpleFunc.integral f := by
+  apply ContinuousLinearMap.extend_eq _ _ simpleFunc.isUniformInducing
+  exact simpleFunc.denseRange one_ne_top
+
+variable (𝕜) in
+theorem integral_eq' (f : α →₁[μ] E) : integral f = integralCLM' 𝕜 f := by
+  apply isClosed_property (simpleFunc.denseRange one_ne_top)
+    (isClosed_eq _ (integralCLM' 𝕜).continuous) _ f
+  · simp_rw [integral_def]
+    exact (integralCLM (E := E)).continuous
+  intro f
+  norm_cast
+
 variable (α E)
 
 @[simp]
@@ -580,9 +594,7 @@ theorem integral_sub (f g : α →₁[μ] E) : integral (f - g) = integral f - i
 
 @[integral_simps]
 theorem integral_smul (c : 𝕜) (f : α →₁[μ] E) : integral (c • f) = c • integral f := by
-  simp only [integral]
-  change (integralCLM' 𝕜) (c • f) = c • (integralCLM' 𝕜) f
-  exact map_smul (integralCLM' 𝕜) c f
+  rw [integral_eq' 𝕜 f, integral_eq' 𝕜 (c • f), map_smul (integralCLM' 𝕜) c f]
 
 theorem norm_Integral_le_one : ‖integralCLM (α := α) (E := E) (μ := μ)‖ ≤ 1 :=
   norm_setToL1_le (dominatedFinMeasAdditive_weightedSMul μ) zero_le_one