theorem
exists_of_convex
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[SigmaCompactSpace M]
[T2Space M]
{F : Type u_5}
[AddCommGroup F]
[Module ℝ F]
{P : (x : M) × (nhds x).Germ F → Prop}
(hP : ∀ (x : M), ReallyConvex ↥(smoothGerm I x) {φ : (nhds x).Germ F | P ⟨x, φ⟩})
(hP' : ∀ (x : M), ∃ (f : M → F), ∀ᶠ (x' : M) in nhds x, P ⟨x', ↑f⟩)
:
theorem
reallyConvex_contMDiffAt
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners ℝ E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(x : M)
(n : ℕ∞)
:
ReallyConvex ↥(smoothGerm I x) {φ : (nhds x).Germ F | Filter.Germ.ContMDiffAt I φ ↑n}
theorem
exists_contMDiff_of_convex
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners ℝ E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
[SigmaCompactSpace M]
[T2Space M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{P : M → F → Prop}
(hP : ∀ (x : M), Convex ℝ {y : F | P x y})
{n : ℕ∞}
(hP' : ∀ (x : M), ∃ U ∈ nhds x, ∃ (f : M → F), ContMDiffOn I (modelWithCornersSelf ℝ F) (↑n) f U ∧ ∀ x ∈ U, P x (f x))
:
∃ (f : M → F), ContMDiff I (modelWithCornersSelf ℝ F) (↑n) f ∧ ∀ (x : M), P x (f x)
theorem
exists_contDiff_of_convex
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{P : E → F → Prop}
(hP : ∀ (x : E), Convex ℝ {y : F | P x y})
{n : ℕ∞}
(hP' : ∀ (x : E), ∃ U ∈ nhds x, ∃ (f : E → F), ContDiffOn ℝ (↑n) f U ∧ ∀ x ∈ U, P x (f x))
:
theorem
reallyConvex_contMDiffAtProd
{E₁ : Type u_1}
{E₂ : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E₁]
[NormedSpace ℝ E₁]
[NormedAddCommGroup E₂]
[NormedSpace ℝ E₂]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H₁ : Type u_4}
{M₁ : Type u_5}
{H₂ : Type u_6}
{M₂ : Type u_7}
[TopologicalSpace H₁]
(I₁ : ModelWithCorners ℝ E₁ H₁)
[TopologicalSpace M₁]
[ChartedSpace H₁ M₁]
[TopologicalSpace H₂]
(I₂ : ModelWithCorners ℝ E₂ H₂)
[TopologicalSpace M₂]
[ChartedSpace H₂ M₂]
{x : M₁}
(n : ℕ∞)
:
ReallyConvex ↥(smoothGerm I₁ x) {φ : (nhds x).Germ (M₂ → F) | Filter.Germ.ContMDiffAtProd I₁ I₂ φ n}
theorem
exists_contMDiff_of_convex₂
{E₁ : Type u_1}
{E₂ : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E₁]
[NormedSpace ℝ E₁]
[FiniteDimensional ℝ E₁]
[NormedAddCommGroup E₂]
[NormedSpace ℝ E₂]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H₁ : Type u_4}
{M₁ : Type u_5}
{H₂ : Type u_6}
{M₂ : Type u_7}
[TopologicalSpace H₁]
(I₁ : ModelWithCorners ℝ E₁ H₁)
[TopologicalSpace M₁]
[ChartedSpace H₁ M₁]
[IsManifold I₁ (↑⊤) M₁]
[TopologicalSpace H₂]
(I₂ : ModelWithCorners ℝ E₂ H₂)
[TopologicalSpace M₂]
[ChartedSpace H₂ M₂]
{P : M₁ → (M₂ → F) → Prop}
[SigmaCompactSpace M₁]
[T2Space M₁]
(hP : ∀ (x : M₁), Convex ℝ {f : M₂ → F | P x f})
{n : ℕ∞}
(hP' :
∀ (x : M₁),
∃ U ∈ nhds x,
∃ (f : M₁ → M₂ → F),
ContMDiffOn (I₁.prod I₂) (modelWithCornersSelf ℝ F) (↑n) (Function.uncurry f) (U ×ˢ Set.univ) ∧ ∀ y ∈ U, P y (f y))
:
∃ (f : M₁ → M₂ → F), ContMDiff (I₁.prod I₂) (modelWithCornersSelf ℝ F) (↑n) (Function.uncurry f) ∧ ∀ (x : M₁), P x (f x)
theorem
exists_contDiff_of_convex₂
{E₁ : Type u_1}
{E₂ : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E₁]
[NormedSpace ℝ E₁]
[FiniteDimensional ℝ E₁]
[NormedAddCommGroup E₂]
[NormedSpace ℝ E₂]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{P : E₁ → (E₂ → F) → Prop}
(hP : ∀ (x : E₁), Convex ℝ {f : E₂ → F | P x f})
{n : ℕ∞}
(hP' :
∀ (x : E₁),
∃ U ∈ nhds x, ∃ (f : E₁ → E₂ → F), ContDiffOn ℝ (↑n) (Function.uncurry f) (U ×ˢ Set.univ) ∧ ∀ y ∈ U, P y (f y))
:
∃ (f : E₁ → E₂ → F), ContDiff ℝ (↑n) (Function.uncurry f) ∧ ∀ (x : E₁), P x (f x)
theorem
convex_setOf_imp_eq
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(P : Prop)
(y : F)
:
theorem
exists_smooth_and_eqOn
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{n : ℕ∞}
{f : E → F}
{ε : E → ℝ}
(hf : Continuous f)
(hε : Continuous ε)
(h2ε : ∀ (x : E), 0 < ε x)
{s : Set E}
(hs : IsClosed s)
(hfs : ∃ U ∈ nhdsSet s, ContDiffOn ℝ (↑n) f U)
: