feat(analysis/calculus): Lagrange multipliers (#6431)

src/algebra/module/linear_map.lean

@@ -165,8 +165,7 @@ def to_add_monoid_hom : M →+ M₂ :=
   map_zero' := f.map_zero,
   map_add' := f.map_add }
 
-@[simp] lemma to_add_monoid_hom_coe :
-  (f.to_add_monoid_hom : M → M₂) = f := rfl
+@[simp] lemma to_add_monoid_hom_coe : ⇑f.to_add_monoid_hom = f := rfl
 
 variable (R)
 

src/analysis/calculus/lagrange_multipliers.lean

@@ -0,0 +1,125 @@
+/-
+Copyright (c) 2021 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Yury Kudryashov
+-/
+import analysis.calculus.local_extr
+import analysis.calculus.implicit
+
+/-!
+# Lagrange multipliers
+
+In this file we formalize the
+[Lagrange multipliers](https://en.wikipedia.org/wiki/Lagrange_multiplier) method of solving
+conditional extremum problems: if a function `φ` has a local extremum at `x₀` on the set
+`f ⁻¹' {f x₀}`, `f x = (f₀ x, ..., fₙ₋₁ x)`, then the differentials of `fₖ` and `φ` are linearly
+dependent. First we formulate a geometric version of this theorem which does not rely on the
+target space being `ℝⁿ`, then restate it in terms of coordinates.
+
+## TODO
+
+Formalize Karush-Kuhn-Tucker theorem
+
+## Tags
+
+lagrange multiplier, local extremum
+
+-/
+
+open filter set
+open_locale topological_space filter big_operators
+variables {E F : Type*} [normed_group E] [normed_space ℝ E] [complete_space E]
+  [normed_group F] [normed_space ℝ F] [complete_space F]
+  {f : E → F} {φ : E → ℝ} {x₀ : E} {f' : E →L[ℝ] F} {φ' : E →L[ℝ] ℝ}
+
+/-- Lagrange multipliers theorem: if `φ : E → ℝ` has a local extremum on the set `{x | f x = f x₀}`
+at `x₀`, both `f : E → F` and `φ` are strictly differentiable at `x₀`, and the codomain of `f` is
+a complete space, then the linear map `x ↦ (f' x, φ' x)` is not surjective. -/
+lemma is_local_extr_on.range_ne_top_of_has_strict_fderiv_at
+  (hextr : is_local_extr_on φ {x | f x = f x₀} x₀) (hf' : has_strict_fderiv_at f f' x₀)
+  (hφ' : has_strict_fderiv_at φ φ' x₀) :
+  (f'.prod φ').range ≠ ⊤ :=
+begin
+  intro htop,
+  set fφ := λ x, (f x, φ x),
+  have A : map φ (𝓝[f ⁻¹' {f x₀}] x₀) = 𝓝 (φ x₀),
+  { change map (prod.snd ∘ fφ) (𝓝[fφ ⁻¹' {p | p.1 = f x₀}] x₀) = 𝓝 (φ x₀),
+    rw [← map_map, nhds_within, map_inf_principal_preimage,
+      (hf'.prod hφ').map_nhds_eq_of_surj htop],
+    exact map_snd_nhds_within _ },
+  exact hextr.not_nhds_le_map A.ge
+end
+
+/-- Lagrange multipliers theorem: if `φ : E → ℝ` has a local extremum on the set `{x | f x = f x₀}`
+at `x₀`, both `f : E → F` and `φ` are strictly differentiable at `x₀`, and the codomain of `f` is
+a complete space, then there exist `Λ : dual ℝ F` and `Λ₀ : ℝ` such that `(Λ, Λ₀) ≠ 0` and
+`Λ (f' x) + Λ₀ • φ' x = 0` for all `x`. -/
+lemma is_local_extr_on.exists_linear_map_of_has_strict_fderiv_at
+  (hextr : is_local_extr_on φ {x | f x = f x₀} x₀) (hf' : has_strict_fderiv_at f f' x₀)
+  (hφ' : has_strict_fderiv_at φ φ' x₀) :
+  ∃ (Λ : module.dual ℝ F) (Λ₀ : ℝ), (Λ, Λ₀) ≠ 0 ∧ ∀ x, Λ (f' x) + Λ₀ • φ' x = 0 :=
+begin
+  rcases submodule.exists_le_ker_of_lt_top _
+    (lt_top_iff_ne_top.2 $ hextr.range_ne_top_of_has_strict_fderiv_at hf' hφ') with ⟨Λ', h0, hΛ'⟩,
+  set e : ((F →ₗ[ℝ] ℝ) × ℝ) ≃ₗ[ℝ] (F × ℝ →ₗ[ℝ] ℝ) :=
+    ((linear_equiv.refl ℝ (F →ₗ[ℝ] ℝ)).prod (linear_map.ring_lmap_equiv_self ℝ ℝ ℝ).symm).trans
+      (linear_map.coprod_equiv ℝ),
+  rcases e.surjective Λ' with ⟨⟨Λ, Λ₀⟩, rfl⟩,
+  refine ⟨Λ, Λ₀, e.map_ne_zero_iff.1 h0, λ x, _⟩,
+  convert linear_map.congr_fun (linear_map.range_le_ker_iff.1 hΛ') x using 1,
+  -- squeezed `simp [mul_comm]` to speed up elaboration
+  simp only [linear_map.coprod_equiv_apply, linear_equiv.refl_apply,
+    linear_map.ring_lmap_equiv_self_symm_apply, linear_map.comp_apply,
+    continuous_linear_map.coe_coe, continuous_linear_map.prod_apply,
+    linear_equiv.trans_apply, linear_equiv.prod_apply, linear_map.coprod_apply,
+    linear_map.smul_right_apply, linear_map.one_app, smul_eq_mul, mul_comm]
+end
+
+/-- Lagrange multipliers theorem. Let `f : ι → E → ℝ` be a finite family of functions.
+Suppose that `φ : E → ℝ` has a local extremum on the set `{x | ∀ i, f i x = f i x₀}` at `x₀`.
+Suppose that all functions `f i` as well as `φ` are strictly differentiable at `x₀`.
+Then the derivatives `f' i : E → L[ℝ] ℝ` and `φ' : E →L[ℝ] ℝ` are linearly dependent:
+there exist `Λ : ι → ℝ` and `Λ₀ : ℝ`, `(Λ, Λ₀) ≠ 0`, such that `∑ i, Λ i • f' i + Λ₀ • φ' = 0`.
+
+See also `is_local_extr_on.linear_dependent_of_has_strict_fderiv_at` for a version that
+states `¬linear_independent ℝ _` instead of existence of `Λ` and `Λ₀`. -/
+lemma is_local_extr_on.exists_multipliers_of_has_strict_fderiv_at {ι : Type*} [fintype ι]
+  {f : ι → E → ℝ} {f' : ι → E →L[ℝ] ℝ}
+  (hextr : is_local_extr_on φ {x | ∀ i, f i x = f i x₀} x₀)
+  (hf' : ∀ i, has_strict_fderiv_at (f i) (f' i) x₀)
+  (hφ' : has_strict_fderiv_at φ φ' x₀) :
+  ∃ (Λ : ι → ℝ) (Λ₀ : ℝ), (Λ, Λ₀) ≠ 0 ∧ ∑ i, Λ i • f' i + Λ₀ • φ' = 0 :=
+begin
+  letI := classical.dec_eq ι,
+  replace hextr : is_local_extr_on φ {x | (λ i, f i x) = (λ i, f i x₀)} x₀,
+    by simpa only [function.funext_iff] using hextr,
+  rcases hextr.exists_linear_map_of_has_strict_fderiv_at
+    (has_strict_fderiv_at_pi.2 (λ i, hf' i)) hφ'
+    with ⟨Λ, Λ₀, h0, hsum⟩,
+  rcases (linear_equiv.pi_ring ℝ ℝ ι ℝ).symm.surjective Λ with ⟨Λ, rfl⟩,
+  refine ⟨Λ, Λ₀, _, _⟩,
+  { simpa only [ne.def, prod.ext_iff, linear_equiv.map_eq_zero_iff, prod.fst_zero] using h0 },
+  { ext x, simpa [mul_comm] using hsum x }
+end
+
+/-- Lagrange multipliers theorem. Let `f : ι → E → ℝ` be a finite family of functions.
+Suppose that `φ : E → ℝ` has a local extremum on the set `{x | ∀ i, f i x = f i x₀}` at `x₀`.
+Suppose that all functions `f i` as well as `φ` are strictly differentiable at `x₀`.
+Then the derivatives `f' i : E → L[ℝ] ℝ` and `φ' : E →L[ℝ] ℝ` are linearly dependent.
+
+See also `is_local_extr_on.exists_multipliers_of_has_strict_fderiv_at` for a version that
+that states existence of Lagrange multipliers `Λ` and `Λ₀` instead of using
+`¬linear_independent ℝ _` -/
+lemma is_local_extr_on.linear_dependent_of_has_strict_fderiv_at {ι : Type*} [fintype ι]
+  {f : ι → E → ℝ} {f' : ι → E →L[ℝ] ℝ}
+  (hextr : is_local_extr_on φ {x | ∀ i, f i x = f i x₀} x₀)
+  (hf' : ∀ i, has_strict_fderiv_at (f i) (f' i) x₀)
+  (hφ' : has_strict_fderiv_at φ φ' x₀) :
+  ¬linear_independent ℝ (λ i, option.elim i φ' f' : option ι → E →L[ℝ] ℝ) :=
+begin
+  rw [fintype.linear_independent_iff], push_neg,
+  rcases hextr.exists_multipliers_of_has_strict_fderiv_at hf' hφ' with ⟨Λ, Λ₀, hΛ, hΛf⟩,
+  refine ⟨λ i, option.elim i Λ₀ Λ, _, _⟩,
+  { simpa [add_comm] using hΛf },
+  { simpa [function.funext_iff, not_and_distrib, or_comm, option.exists] using hΛ }
+end

src/data/fintype/card.lean

@@ -81,7 +81,15 @@ open finset
 
 section
 
-variables {M : Type*} [fintype α] [decidable_eq α] [comm_monoid M]
+variables {M : Type*} [fintype α] [comm_monoid M]
+
+@[simp, to_additive]
+lemma fintype.prod_option (f : option α → M) : ∏ i, f i = f none * ∏ i, f (some i) :=
+show ((finset.insert_none _).1.map f).prod = _,
+by simp only [finset.prod, finset.insert_none, multiset.map_cons, multiset.prod_cons,
+  multiset.map_map]
+
+variable [decidable_eq α]
 
 @[to_additive]
 lemma is_compl.prod_mul_prod {s t : finset α} (h : is_compl s t) (f : α → M) :

src/linear_algebra/basic.lean

@@ -354,7 +354,7 @@ This says that the forgetful functor from `R`-modules to types is representable,
 
 This as an `S`-linear equivalence, under the assumption that `S` acts on `M` commuting with `R`.
 When `R` is commutative, we can take this to be the usual action with `S = R`.
-Otherwise, `S = ℤ` shows that the equivalence is additive.
+Otherwise, `S = ℕ` shows that the equivalence is additive.
 See note [bundled maps over different rings].
 -/
 @[simps]

src/linear_algebra/pi.lean

@@ -27,11 +27,11 @@ universes u v w x y z u' v' w' y'
 variables {R : Type u} {K : Type u'} {M : Type v} {V : Type v'} {M₂ : Type w} {V₂ : Type w'}
 variables {M₃ : Type y} {V₃ : Type y'} {M₄ : Type z} {ι : Type x}
 
-namespace linear_map
-
 open function submodule
 open_locale big_operators
 
+namespace linear_map
+
 universe i
 variables [semiring R] [add_comm_monoid M₂] [semimodule R M₂] [add_comm_monoid M₃] [semimodule R M₃]
 {φ : ι → Type i} [∀i, add_comm_monoid (φ i)] [∀i, semimodule R (φ i)]
@@ -86,6 +86,8 @@ def single [decidable_eq ι] (i : ι) : φ i →ₗ[R] (Πi, φ i) :=
 @[simp] lemma coe_single [decidable_eq ι] (i : ι) :
   ⇑(single i : φ i →ₗ[R] (Π i, φ i)) = pi.single i := rfl
 
+variables (R φ)
+
 /-- The linear equivalence between linear functions on a finite product of modules and
 families of functions on these modules. See note [bundled maps over different rings]. -/
 def lsum (S) [add_comm_monoid M] [semimodule R M] [fintype ι] [decidable_eq ι]
@@ -103,6 +105,8 @@ def lsum (S) [add_comm_monoid M] [semimodule R M] [fintype ι] [decidable_eq ι]
       rw finset.univ_sum_single
     end }
 
+variables {R φ}
+
 section ext
 
 variables [fintype ι] [decidable_eq ι] [add_comm_monoid M] [semimodule R M]
@@ -192,4 +196,28 @@ variables [semiring R] {φ ψ : ι → Type*} [∀i, add_comm_monoid (φ i)] [
   left_inv := λ f, by { ext, simp },
   right_inv := λ f, by { ext, simp } }
 
+variables (ι R M) (S : Type*) [fintype ι] [decidable_eq ι] [semiring S]
+  [add_comm_monoid M] [semimodule R M] [semimodule S M] [smul_comm_class R S M]
+
+/-- Linear equivalence between linear functions `Rⁿ → M` and `Mⁿ`. The spaces `Rⁿ` and `Mⁿ`
+are represented as `ι → R` and `ι → M`, respectively, where `ι` is a finite type.
+
+This as an `S`-linear equivalence, under the assumption that `S` acts on `M` commuting with `R`.
+When `R` is commutative, we can take this to be the usual action with `S = R`.
+Otherwise, `S = ℕ` shows that the equivalence is additive.
+See note [bundled maps over different rings]. -/
+def pi_ring : ((ι → R) →ₗ[R] M) ≃ₗ[S] (ι → M) :=
+(linear_map.lsum R (λ i : ι, R) S).symm.trans
+  (pi $ λ i, linear_map.ring_lmap_equiv_self R M S)
+
+variables {ι R M}
+
+@[simp] lemma pi_ring_apply (f : (ι → R) →ₗ[R] M) (i : ι) :
+  pi_ring R M ι S f i = f (pi.single i 1) :=
+rfl
+
+@[simp] lemma pi_ring_symm_apply (f : ι → M) (g : ι → R) :
+  (pi_ring R M ι S).symm f g = ∑ i, g i • f i :=
+by simp [pi_ring, linear_map.lsum]
+
 end linear_equiv

src/order/filter/extr.lean

@@ -120,6 +120,14 @@ univ_subset_iff.trans eq_univ_iff_forall
 lemma is_max_on_univ_iff : is_max_on f univ a ↔ ∀ x, f x ≤ f a :=
 univ_subset_iff.trans eq_univ_iff_forall
 
+lemma is_min_filter.tendsto_principal_Ici (h : is_min_filter f l a) :
+  tendsto f l (𝓟 $ Ici (f a)) :=
+tendsto_principal.2 h
+
+lemma is_max_filter.tendsto_principal_Iic (h : is_max_filter f l a) :
+  tendsto f l (𝓟 $ Iic (f a)) :=
+tendsto_principal.2 h
+
 /-! ### Conversion to `is_extr_*` -/
 
 lemma is_min_filter.is_extr : is_min_filter f l a → is_extr_filter f l a := or.inl

src/topology/algebra/module.lean

@@ -383,13 +383,17 @@ instance : add_comm_monoid (M →L[R] M₂) :=
 by { refine {zero := 0, add := (+), ..}; intros; ext;
   apply_rules [zero_add, add_assoc, add_zero, add_left_neg, add_comm] }
 
+@[simp, norm_cast] lemma coe_sum {ι : Type*} (t : finset ι) (f : ι → M →L[R] M₂) :
+  ↑(∑ d in t, f d) = (∑ d in t, f d : M →ₗ[R] M₂) :=
+(add_monoid_hom.mk (coe : (M →L[R] M₂) → (M →ₗ[R] M₂)) rfl (λ _ _, rfl)).map_sum _ _
+
+@[simp, norm_cast] lemma coe_sum' {ι : Type*} (t : finset ι) (f : ι → M →L[R] M₂) :
+  ⇑(∑ d in t, f d) = ∑ d in t, f d :=
+by simp only [← coe_coe, coe_sum, linear_map.coe_fn_sum]
+
 lemma sum_apply {ι : Type*} (t : finset ι) (f : ι → M →L[R] M₂) (b : M) :
   (∑ d in t, f d) b = ∑ d in t, f d b :=
-begin
-  haveI : is_add_monoid_hom (λ (g : M →L[R] M₂), g b) :=
-    { map_add := λ f g, continuous_linear_map.add_apply f g b, map_zero := by simp },
-  exact (finset.sum_hom t (λ g : M →L[R] M₂, g b)).symm
-end
+by simp only [coe_sum', finset.sum_apply]
 
 end add
 

src/topology/continuous_on.lean

@@ -203,8 +203,7 @@ theorem filter.tendsto.if_nhds_within {f g : α → β} {p : α → Prop} [decid
 h₀.piecewise_nhds_within h₁
 
 lemma map_nhds_within (f : α → β) (a : α) (s : set α) :
-  map f (𝓝[s] a) =
-    ⨅ t ∈ {t : set α | a ∈ t ∧ is_open t}, 𝓟 (set.image f (t ∩ s)) :=
+  map f (𝓝[s] a) = ⨅ t ∈ {t : set α | a ∈ t ∧ is_open t}, 𝓟 (f  '' (t ∩ s)) :=
 ((nhds_within_basis_open a s).map f).eq_binfi
 
 theorem tendsto_nhds_within_mono_left {f : α → β} {a : α}