mderiv.lean

/-
Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sébastien Gouëzel

Manifolds based on any structure groupoid of homeomorphisms.

long term TODO:
*  ≤ on groupoids, interfaced with type classes, to say that a C^k manifold is automatically
a C^1 manifold when 1 ≤ k
*  Oriented manifolds, with orientation preserving structure groupoid
*  definition of C^k regularity classes, and C^k manifolds
*  tangent bundle of a C^k manifold, as a C^{k-1} manifold
*  any C^1 manifold admits a C^∞ structure (would require some integration to define convolution)
*  any two C^∞ structures on a C^1 manifold are diffeomorphic
*  Whitney (weak version): any C^k real manifold embeds in ℝ^N for large enough N
*  submanifolds, embeddings, and so on
-/

import geometry.manifolds.manifold

noncomputable theory
local attribute [instance, priority 0] classical.decidable_inhabited classical.prop_decidable

section tangent_space
open manifold set

local infixr  ` →ₕ `:100 := local_homeomorph.trans

/- Specialization to the case of smooth manifolds, over a field k and with a smoothness n.
The set E is a vector space, and H is a model with boundary based on E.
When n and k are fixed, the model space with boundary (H, E) should always be the same for a
given manifold M. Therefore, we register it as an out_param: it will not be necessary to write
it out explicitely when talking about smooth manifolds. This is the main point of this definition. -/
class manifold.smooth (n : with_top ℕ) (k : Type*) [nondiscrete_normed_field k]
  (E : out_param $ Type*) [out_param $ normed_space k E] (H : out_param $ Type*)
  [out_param $ topological_space H] (I : out_param $ model_with_boundary k E H)
  (M : Type*) [topological_space M] [out_param $ manifold H M] extends
  manifold.has_groupoid H M (times_cont_diff_groupoid n k E H I)

/-- The model space is the simplest example of a smooth manifold -/
instance model_space_smooth (n : with_top ℕ) (k : Type*) [nondiscrete_normed_field k]
  (E : Type*) [normed_space k E] : manifold.smooth n k E E (model_with_boundary_self k E) E := {}


section extended_charts

variables (k : Type*) [nondiscrete_normed_field k]
  {E : Type*} [normed_space k E]
  {H : Type*} [topological_space H] {I : model_with_boundary k E H}
  {M : Type*} [topological_space M] [manifold H M]
  [manifold.smooth 1 k E H I M]
  (x : M) {s t : set M}

include k E H I M

/- In a smooth manifold with boundary, the model space is the space H. However, we will also
need to use extended charts taking values in the model vector space E. These extended charts are
not `local_homeomorph` as the target is not open in E in general, but we can still register them
as `local_equiv` -/

def ext_chart_at : local_equiv M E :=
(some_chart_at H x).to_local_equiv.trans I.to_local_equiv

lemma ext_chart_at_source : (ext_chart_at k x).source = (some_chart_at H x).source :=
by rw [ext_chart_at, local_equiv.trans_source, I.source_eq, preimage_univ, inter_univ]

lemma ext_chart_at_open_source : is_open (ext_chart_at k x).source :=
by { rw ext_chart_at_source, exact (some_chart_at H x).open_source }

lemma mem_ext_chart_at_source : x ∈ (ext_chart_at k x).source :=
by { rw ext_chart_at_source, exact mem_some_chart_at_source _ _ }

lemma ext_chart_at_source_mem_nhds : (ext_chart_at k x).source ∈ nhds x :=
mem_nhds_sets (ext_chart_at_open_source k x) (mem_ext_chart_at_source k x)

lemma ext_chart_at_continuous_on_to_fun :
  continuous_on (ext_chart_at k x).to_fun (ext_chart_at k x).source :=
begin
  refine continuous_on.comp I.continuous_to_fun.continuous_on _ (subset_univ _),
  rw ext_chart_at_source,
  exact (some_chart_at H x).continuous_to
end

lemma ext_chart_at_continuous_at_to_fun :
  continuous_at (ext_chart_at k x).to_fun x :=
(ext_chart_at_continuous_on_to_fun k x x (mem_ext_chart_at_source k x)).continuous_at
  (ext_chart_at_source_mem_nhds k x)

lemma ext_chart_at_continuous_on_inv_fun : continuous_on (ext_chart_at k x).inv_fun (ext_chart_at k x).target :=
begin
  apply continuous_on.comp (some_chart_at H x).continuous_inv,
  apply I.continuous_inv_fun.continuous_on,
  unfold ext_chart_at,
  rw [local_equiv.restr_inv_fun, local_equiv.image_trans_target],
  exact inter_subset_right _ _
end

lemma ext_chart_at_target_mem_nhds_within :
  (ext_chart_at k x).target ∈ nhds_within ((ext_chart_at k x).to_fun x) (range I.to_fun) :=
begin
  rw [ext_chart_at, local_equiv.trans_target],
  simp only [function.comp_app, local_equiv.trans_to_fun, model_with_boundary_target],
  refine inter_mem_nhds_within _
    (mem_nhds_sets (I.continuous_inv_fun _ (some_chart_at H x).open_target) _),
  simp only [mem_preimage_eq, model_with_boundary_inv_fun_to_fun],
  exact (some_chart_at H x).to_map _ (mem_some_chart_at_source _ _),
end

lemma nhds_within_ext_chart_target_eq :
  nhds_within ((ext_chart_at k x).to_fun x) (ext_chart_at k x).target =
  nhds_within ((ext_chart_at k x).to_fun x) (range I.to_fun) :=
begin
  apply le_antisymm,
  { apply nhds_within_mono,
    simp [ext_chart_at, local_equiv.trans_target] },
  { apply nhds_within_le_of_mem (ext_chart_at_target_mem_nhds_within _ _) }
end

lemma ext_chart_continuous_at_inv_fun :
  continuous_at (ext_chart_at k x).inv_fun ((ext_chart_at k x).to_fun x) :=
begin
  apply continuous_at.comp,
  { simp [ext_chart_at],
    exact ((some_chart_at H x).continuous_inv _
      ((some_chart_at H x).to_map _ (mem_some_chart_at_source _ _))).continuous_at
        (mem_nhds_sets (some_chart_at H x).open_target
          ((some_chart_at H x).to_map _ (mem_some_chart_at_source _ _))) },
  { exact I.continuous_inv_fun.continuous_at }
end

/-- Technical lemma ensuring that the preimage under a chart of a neighborhood of a point
is a neighborhood of the preimage, within a set. -/
lemma ext_chart_preimage_mem_nhds_within (ht : t ∈ nhds_within x s) :
  (ext_chart_at k x).inv_fun ⁻¹' t ∈ nhds_within ((ext_chart_at k x).to_fun x)
    ((ext_chart_at k x).inv_fun ⁻¹' s ∩ range I.to_fun) :=
begin
  apply (ext_chart_continuous_at_inv_fun k x).continuous_within_at.tendsto_nhds_within_image,
  rw (ext_chart_at k x).to_inv _ (mem_ext_chart_at_source _ _),
  apply nhds_within_mono _ _ ht,
  have : (ext_chart_at k x).inv_fun '' ((ext_chart_at k x).inv_fun ⁻¹' s) ⊆ s :=
    image_preimage_subset _ _,
  exact subset.trans (image_subset _ (inter_subset_left _ _)) this
end

/-- Technical lemma ensuring that the preimage under a chart of a neighborhood of a point
is a neighborhood of the preimage. -/
lemma ext_chart_preimage_mem_nhds (ht : t ∈ nhds x) :
  (ext_chart_at k x).inv_fun ⁻¹' t ∈ nhds ((ext_chart_at k x).to_fun x) :=
begin
  apply (ext_chart_continuous_at_inv_fun k x).preimage_mem_nhds,
  rwa (ext_chart_at k x).to_inv _ (mem_ext_chart_at_source _ _)
end

/-- Technical lemma to rewrite suitably the preimage of an intersection under a chart, to bring
it into a convenient form to apply derivative lemmas. -/
lemma ext_chart_preimage_inter_eq : ((ext_chart_at k x).inv_fun ⁻¹' (s ∩ t) ∩ range I.to_fun)
  = ((ext_chart_at k x).inv_fun ⁻¹' s ∩ range (I.to_fun))
    ∩ ((ext_chart_at k x).inv_fun ⁻¹' t) :=
begin
  rw [preimage_inter, inter_assoc, inter_assoc],
  congr' 1,
  rw inter_comm
end

end extended_charts

/- In the next definition, E, H and I can be implicit thanks to the out_param in manifold.smooth.
There are many equivalent mathematical ways to define the tangent space to a manifold. One should
get a vector space isomorphic to E, and the organize them in the tangent bundle to get a locally
trivial vector bundle. A canonical definition in the case of manifolds over ℝ is to consider the
set of derivations acting on C^1 functions. Another canonical definition is to take all pairs
(e, E) where e is a chart at x, and identify two of these spaces by the derivative of e' ∘ e^{-1},
to get a canonical vector space.
These approaches give canonical vector spaces, but no norm on them (in the second example, one can
get a family of norms, one corresponding to each chart, and they are all equivalent so they define
the same topology, but to get a norm one has to make an arbitrary choice). Since we want a norm
(to be able to talk about bounded linear maps between tangent spaces), we follow a less canonical
route: at each point x, we choose some arbitrary chart `some_chart_at H x`, and define the tangent
space to be the model space `E` (with the idea that in fact we want to use
`(inj ∘ some_chart at H x)^* E`). This has several practical advantages:
* without any work, one gets a normed vector space structure on the tangent space
* in the case of the vector space model space (where `some_chart_at E x` has to be the identity
since this is the only chart), one gets back the canonical identification between the tangent space
to the model space E and the space E itself, in a defeq way (contrary to what the other
constructions would give). This means that the derivative in the manifold sense is really equal
to the usual derivative.

A drawback is that some silly constructions will typecheck: one can add two vectors in different
tangent spaces (as they both are elements of E from the point of view of Lean). To solve this, one
could mark the tangent space as irreducible, but then one would lose the identification of the
tangent space to E with E.
 -/


/-- The tangent space at a smooth manifold `M` over the field `k` and the model with boundary (H, E).
The model space with boundary (H, E) is implicit, while the field `k` is explicit as we may consider
some manifolds both as a real and complex manifold. We use `E` for a model of the tangent space,
through one choice of a chart around `x`. The smoothness typeclass assumption is relevant to allow
(E, H, I) to be implicit through the `out_param` in the definition of `manifold.smooth`. -/
def tangent_space_at (k : Type*) [nondiscrete_normed_field k]
  {E : Type*} [normed_space k E]
  {H : Type*} [topological_space H] {I : model_with_boundary k E H}
  {M : Type*} [topological_space M] [manifold H M]
  [manifold.smooth 1 k E H I M]
  (x : M) : Type* := E

section tangent_space_at_structure
/- Register the normed vector space structure on the tangent space, -/
local attribute [reducible] tangent_space_at

instance (k : Type*) [nondiscrete_normed_field k]
  {E : Type*} [normed_space k E]
  {H : Type*} [topological_space H] {I : model_with_boundary k E H}
  {M : Type*} [topological_space M] [manifold H M]
  [manifold.smooth 1 k E H I M]
  (x : M) : normed_space k (tangent_space_at k x) := by apply_instance

end tangent_space_at_structure

/-- The tangent bundle to a smooth manifold over a field k -/
def tangent_bundle (k : Type) [nondiscrete_normed_field k]
  {E : Type} [normed_space k E]
  {H : Type*} [topological_space H] {I : model_with_boundary k E H}
  (M : Type*) [topological_space M] [manifold H M]
  [manifold.smooth 1 k E H I M] : Type* :=
(Σx:M, tangent_space_at k x)

/-- The base projection from the tangent bundle to the underlying manifold -/
def tangent_bundle_proj (k : Type) [nondiscrete_normed_field k]
  {E : Type} [normed_space k E]
  {H : Type*} [topological_space H] {I : model_with_boundary k E H}
  (M : Type*) [topological_space M] [manifold H M] [manifold.smooth 1 k E H I M] :
  tangent_bundle k M → M :=
λp, p.1

section derivatives_definitions
/- The derivative of a smooth map f between smooth manifold M and M' at x is a bounded linear map
from the tangent space to M at x, to the tangent space to M' at f x. Since we defined the tangent
space using one specific chart, the formula for the derivative is written in terms of this
specific chart.

We use the names mdifferentiable and mfderiv, where the prefix letter m means "manifold".
-/

variables (k : Type) [nondiscrete_normed_field k]
{E : Type*} [normed_space k E]
{H : Type*} [topological_space H] {I : model_with_boundary k E H}
{M : Type*} [topological_space M] [manifold H M] [manifold.smooth 1 k E H I M]
{E' : Type} [normed_space k E']
{H' : Type*} [topological_space H'] {I' : model_with_boundary k E' H'}
{M' : Type*} [topological_space M'] [manifold H' M'] [manifold.smooth 1 k E' H' I' M']

include E H I M

def unique_mdiff_within_at (s : set M) (x : M) :=
unique_diff_within_at k ((ext_chart_at k x).inv_fun ⁻¹' s ∩ range I.to_fun)
  ((ext_chart_at k x).to_fun x)

def unique_mdiff_on (s : set M) :=
∀x∈s, unique_mdiff_within_at k s x

include E' H' I' M'

def written_in_ext_chart_at (x : M) (f : M → M') : E → E' :=
(ext_chart_at k (f x)).to_fun ∘ f ∘ (ext_chart_at k x).inv_fun

/- In the next two definitions, the information about k is contained in the type of f', hence
it can be made implicit. -/
variable {k}

/-- generalization of `has_fderiv_within_at` to manifolds (as indicated by the prefix `m`).
The order of arguments is changed as the type of the derivative `f'` depends on the choice of
`x`. This only makes sense if the function is continuous within s at x, as otherwise the function
read in charts does not make sense as one can not use one single chart for the image. Hence, we need
to add continuous_within_at as an assumption. Otherwise, this is the same definition read in charts. -/
def has_mfderiv_within_at (f : M → M') (s : set M) (x : M)
  (f' : tangent_space_at k x →L[k] tangent_space_at k (f x)) :=
continuous_within_at f s x ∧
has_fderiv_within_at (written_in_ext_chart_at k x f) f'
  ((ext_chart_at k x).inv_fun ⁻¹' s ∩ range I.to_fun) ((ext_chart_at k x).to_fun x)

/-- generalization of `has_fderiv_at` to manifolds (as indicated by the prefix `m`).
The order of arguments is changed as the type of the derivative `f'` depends on the choice of
`x`. This only makes sense if the function is continuous at x, as otherwise the function
read in charts does not make sense as one can not use one single chart for the image. Hence, we need
to add continuous_at as an assumption. Otherwise, this is the same definition read in charts. -/
def has_mfderiv_at (f : M → M') (x : M)
  (f' : tangent_space_at k x →L[k] tangent_space_at k (f x)) :=
continuous_at f x ∧
has_fderiv_within_at (written_in_ext_chart_at k x f) f' (range I.to_fun) ((ext_chart_at k x).to_fun x)

variable (k)

def mdifferentiable_within_at (f : M → M') (s : set M) (x : M) :=
continuous_within_at f s x ∧
differentiable_within_at k (written_in_ext_chart_at k x f)
  ((ext_chart_at k x).inv_fun ⁻¹' s ∩ range I.to_fun) ((ext_chart_at k x).to_fun x)

def mdifferentiable_at (f : M → M') (x : M) :=
continuous_at f x ∧
differentiable_within_at k (written_in_ext_chart_at k x f) (range I.to_fun)
  ((ext_chart_at k x).to_fun x)

def mfderiv_within (f : M → M') (s : set M) (x : M) :
  tangent_space_at k x →L[k] tangent_space_at k (f x) :=
fderiv_within k (written_in_ext_chart_at k x f) ((ext_chart_at k x).inv_fun ⁻¹' s ∩ range I.to_fun)
  ((ext_chart_at k x).to_fun x)

def mfderiv (f : M → M') (x : M) :
  tangent_space_at k x →L[k] tangent_space_at k (f x) :=
fderiv_within k (written_in_ext_chart_at k x f) (range I.to_fun) ((ext_chart_at k x).to_fun x)

def mdifferentiable_on (f : M → M') (s : set M) :=
∀x ∈ s, mdifferentiable_within_at k f s x

def mdifferentiable (f : M → M') :=
∀x, mdifferentiable_at k f x

end derivatives_definitions

section derivatives_properties

variables {k : Type} [nondiscrete_normed_field k]
{E : Type*} [normed_space k E]
{H : Type*} [topological_space H] {I : model_with_boundary k E H}
{M : Type*} [topological_space M] [manifold H M] [manifold.smooth 1 k E H I M]
{E' : Type} [normed_space k E']
{H' : Type*} [topological_space H'] {I' : model_with_boundary k E' H'}
{M' : Type*} [topological_space M'] [manifold H' M'] [manifold.smooth 1 k E' H' I' M']
{E'' : Type} [normed_space k E'']
{H'' : Type*} [topological_space H''] {I'' : model_with_boundary k E'' H''}
{M'' : Type*} [topological_space M''] [manifold H'' M''] [manifold.smooth 1 k E'' H'' I'' M'']
{f f₀ f₁ : M → M'}
{x : M}
{f' f₀' f₁' : tangent_space_at k x →L[k] tangent_space_at k (f x)}
{s t : set M}
{g : M' → M''}
{g' : tangent_space_at k (f x) →L[k] tangent_space_at k (g (f x))}
{u : set M'}

include E H I M

/- Lemmas on unique_mdiff -/

/-- `unique_mdiff_within_at` achieves its goal: it implies the uniqueness of the derivative. -/
theorem unique_mdiff_within_at.eq (U : unique_mdiff_within_at k s x)
  (h : has_mfderiv_within_at f s x f') (h₁ : has_mfderiv_within_at f s x f₁') : f' = f₁' :=
U.eq h.2 h₁.2

theorem unique_mdiff_on.eq (U : unique_mdiff_on k s) (hx : x ∈ s)
  (h : has_mfderiv_within_at f s x f') (h₁ : has_mfderiv_within_at f s x f₁') : f' = f₁' :=
unique_mdiff_within_at.eq (U x hx) h h₁

lemma unique_mdiff_within_at_univ : unique_mdiff_within_at k univ x :=
begin
  unfold unique_mdiff_within_at,
  simp,
  exact I.unique_diff _ (mem_range_self _)
end

lemma unique_mdiff_within_at.mono (h : unique_mdiff_within_at k s x) (st : s ⊆ t) :
  unique_mdiff_within_at k t x :=
unique_diff_within_at.mono h $ inter_subset_inter (preimage_mono st) (subset.refl _)

lemma unique_mdiff_within_at_inter (hs : unique_mdiff_within_at k s x) (ht : t ∈ nhds x) :
  unique_mdiff_within_at k (s ∩ t) x :=
begin
  rw [unique_mdiff_within_at, ext_chart_preimage_inter_eq],
  exact unique_diff_within_at_inter hs (ext_chart_preimage_mem_nhds k x ht)
end

lemma is_open.unique_mdiff_within_at (xs : x ∈ s) (hs : is_open s) : unique_mdiff_within_at k s x :=
begin
  have := unique_mdiff_within_at_inter unique_mdiff_within_at_univ (mem_nhds_sets hs xs),
  rwa univ_inter at this
end

lemma unique_mdiff_on_inter (hs : unique_mdiff_on k s) (ht : is_open t) : unique_mdiff_on k (s ∩ t) :=
λx hx, unique_mdiff_within_at_inter (hs x hx.1) (mem_nhds_sets ht hx.2)

lemma is_open.unique_mdiff_on (hs : is_open s) : unique_mdiff_on k s :=
λx hx, is_open.unique_mdiff_within_at hx hs

/- General lemmas on derivatives -/

include E' H' I' M'

theorem has_mfderiv_within_at.mono (h : has_mfderiv_within_at f t x f') (hst : s ⊆ t) :
  has_mfderiv_within_at f s x f' :=
⟨ continuous_within_at.mono h.1 hst,
  has_fderiv_within_at.mono h.2 (inter_subset_inter (preimage_mono hst) (subset.refl _)) ⟩

theorem has_mfderiv_at.has_mfderiv_within_at
  (h : has_mfderiv_at f x f') : has_mfderiv_within_at f s x f' :=
⟨ continuous_at.continuous_within_at h.1, has_fderiv_within_at.mono h.2 (inter_subset_right _ _) ⟩

lemma has_mfderiv_within_at.mdifferentiable_within_at (h : has_mfderiv_within_at f s x f') :
  mdifferentiable_within_at k f s x :=
⟨h.1, ⟨f', h.2⟩⟩

lemma has_mfderiv_at.mdifferentiable_at (h : has_mfderiv_at f x f') : mdifferentiable_at k f x :=
⟨h.1, ⟨f', h.2⟩⟩

@[simp] lemma has_mfderiv_within_at_univ :
  has_mfderiv_within_at f univ x f' ↔ has_mfderiv_at f x f' :=
by simp [has_mfderiv_within_at, has_mfderiv_at, continuous_within_at_univ]

theorem has_mfderiv_at_unique
  (h₀ : has_mfderiv_at f x f₀') (h₁ : has_mfderiv_at f x f₁') : f₀' = f₁' :=
begin
  rw ← has_mfderiv_within_at_univ at h₀ h₁,
  exact unique_mdiff_within_at_univ.eq h₀ h₁
end

lemma has_mfderiv_within_at_inter' (h : t ∈ nhds_within x s) :
  has_mfderiv_within_at f (s ∩ t) x f' ↔ has_mfderiv_within_at f s x f' :=
begin
  rw [has_mfderiv_within_at, has_mfderiv_within_at, ext_chart_preimage_inter_eq,
      has_fderiv_within_at_inter', continuous_within_at_inter' h],
  exact ext_chart_preimage_mem_nhds_within k x h,
end

lemma has_mfderiv_within_at_inter (h : t ∈ nhds x) :
  has_mfderiv_within_at f (s ∩ t) x f' ↔ has_mfderiv_within_at f s x f' :=
begin
  rw [has_mfderiv_within_at, has_mfderiv_within_at, ext_chart_preimage_inter_eq,
      has_fderiv_within_at_inter, continuous_within_at_inter h],
  exact ext_chart_preimage_mem_nhds k x h,
end

lemma mdifferentiable_within_at.has_mfderiv_within_at (h : mdifferentiable_within_at k f s x) :
  has_mfderiv_within_at f s x (mfderiv_within k f s x) :=
⟨h.1, differentiable_within_at.has_fderiv_within_at h.2⟩

lemma mdifferentiable_at.has_mfderiv_at (h : mdifferentiable_at k f x) :
  has_mfderiv_at f x (mfderiv k f x) :=
⟨h.1, differentiable_within_at.has_fderiv_within_at h.2⟩

lemma has_mfderiv_at.mfderiv (h : has_mfderiv_at f x f') :
  mfderiv k f x = f' :=
by { ext, rw has_mfderiv_at_unique h h.mdifferentiable_at.has_mfderiv_at }

lemma has_mfderiv_within_at.mfderiv_within
  (h : has_mfderiv_within_at f s x f') (hxs : unique_mdiff_within_at k s x) :
  mfderiv_within k f s x = f' :=
by { ext, rw hxs.eq h h.mdifferentiable_within_at.has_mfderiv_within_at }

lemma mdifferentiable_within_at.mono (hst : s ⊆ t)
  (h : mdifferentiable_within_at k f t x) : mdifferentiable_within_at k f s x :=
⟨ continuous_within_at.mono h.1 hst,
  differentiable_within_at.mono h.2 (inter_subset_inter (preimage_mono hst) (subset.refl _)) ⟩

lemma mdifferentiable_within_at_univ :
  mdifferentiable_within_at k f univ x ↔ mdifferentiable_at k f x :=
by simp [mdifferentiable_within_at, mdifferentiable_at, continuous_within_at_univ]

lemma mdifferentiable_within_at_inter (ht : t ∈ nhds x) :
  mdifferentiable_within_at k f (s ∩ t) x ↔ mdifferentiable_within_at k f s x :=
begin
  rw [mdifferentiable_within_at, mdifferentiable_within_at, ext_chart_preimage_inter_eq,
      differentiable_within_at_inter, continuous_within_at_inter ht],
  exact ext_chart_preimage_mem_nhds k x ht
end

lemma mdifferentiable_at.mdifferentiable_within_at
  (h : mdifferentiable_at k f x) : mdifferentiable_within_at k f s x :=
mdifferentiable_within_at.mono (subset_univ _) (mdifferentiable_within_at_univ.2 h)

lemma mdifferentiable_within_at.mdifferentiable_at
  (h : mdifferentiable_within_at k f s x) (hs : s ∈ nhds x) : mdifferentiable_at k f x :=
begin
  have : s = univ ∩ s, by rw univ_inter,
  rwa [this, mdifferentiable_within_at_inter hs, mdifferentiable_within_at_univ] at h
end

lemma mdifferentiable.mfderiv_within
  (h : mdifferentiable_at k f x) (hxs : unique_mdiff_within_at k s x) :
  mfderiv_within k f s x = mfderiv k f x :=
begin
  apply has_mfderiv_within_at.mfderiv_within _ hxs,
  exact h.has_mfderiv_at.has_mfderiv_within_at
end

lemma mdifferentiable_on.mono
  (h : mdifferentiable_on k f t) (st : s ⊆ t) : mdifferentiable_on k f s :=
λx hx, (h x (st hx)).mono st

lemma mdifferentiable_on_univ :
  mdifferentiable_on k f univ ↔ mdifferentiable k f :=
by { simp [mdifferentiable_on, mdifferentiable_within_at_univ], refl }

lemma mdifferentiable.mdifferentiable_on
  (h : mdifferentiable k f) : mdifferentiable_on k f s :=
(mdifferentiable_on_univ.2 h).mono (subset_univ _)

lemma mdifferentiable_on_of_locally_mdifferentiable_on
  (h : ∀x∈s, ∃u, is_open u ∧ x ∈ u ∧ mdifferentiable_on k f (s ∩ u)) : mdifferentiable_on k f s :=
begin
  assume x xs,
  rcases h x xs with ⟨t, t_open, xt, ht⟩,
  exact (mdifferentiable_within_at_inter (mem_nhds_sets t_open xt)).1 (ht x ⟨xs, xt⟩)
end

lemma mfderiv_within_subset (st : s ⊆ t) (ht : unique_mdiff_within_at k s x)
  (h : mdifferentiable_within_at k f t x) :
  mfderiv_within k f s x = mfderiv_within k f t x :=
((mdifferentiable_within_at.has_mfderiv_within_at h).mono st).mfderiv_within ht

@[simp] lemma mfderiv_within_univ : mfderiv_within k f univ = mfderiv k f :=
by { ext x : 1, simp [mfderiv_within, mfderiv] }

lemma mfderiv_within_inter (ht : t ∈ nhds x) (hs : unique_mdiff_within_at k s x) :
  mfderiv_within k f (s ∩ t) x = mfderiv_within k f s x :=
begin
  rw [mfderiv_within, mfderiv_within],
  erw ext_chart_preimage_inter_eq,
  exact fderiv_within_inter (ext_chart_preimage_mem_nhds k x ht) hs
end

/- Continuity -/

theorem has_mfderiv_within_at.continuous_within_at
  (h : mdifferentiable_within_at k f s x) : continuous_within_at f s x :=
h.1

theorem has_mfderiv_at.continuous_at (h : has_mfderiv_at f x f') :
  continuous_at f x :=
h.1

lemma mdifferentiable_within_at.continuous_within_at (h : mdifferentiable_within_at k f s x) :
  continuous_within_at f s x :=
h.1

lemma mdifferentiable_at.continuous_at (h : mdifferentiable_at k f x) : continuous_at f x :=
h.1

lemma mdifferentiable_on.continuous_on (h : mdifferentiable_on k f s) : continuous_on f s :=
λx hx, (h x hx).continuous_within_at

lemma mdifferentiable.continuous (h : mdifferentiable k f) : continuous f :=
continuous_iff_continuous_at.2 $ λx, (h x).continuous_at

/- Composition lemmas -/

include E'' H'' I'' M''

lemma written_in_ext_chart_comp (h : continuous_within_at f s x) :
  {y | written_in_ext_chart_at k x (g ∘ f) y
       = ((written_in_ext_chart_at k (f x) g) ∘ (written_in_ext_chart_at k x f)) y}
  ∈ nhds_within ((ext_chart_at k x).to_fun x) ((ext_chart_at k x).inv_fun ⁻¹' s ∩ range I.to_fun) :=
begin
  apply @filter.mem_sets_of_superset _ _
    ((f ∘ (ext_chart_at k x).inv_fun)⁻¹' (ext_chart_at k (f x)).source) _
    (ext_chart_preimage_mem_nhds_within k x (h.preimage_mem_nhds_within (ext_chart_at_source_mem_nhds _ _))),
  assume y hy,
  simp only [written_in_ext_chart_at, ext_chart_at, mem_set_of_eq, function.comp_app,
    model_with_boundary_inv_fun_to_fun, local_equiv.trans_to_fun, local_equiv.trans_inv_fun],
  rw (some_chart_at H' (f x)).to_inv,
  simpa [ext_chart_at_source] using hy
end

variable (x)

theorem has_mfderiv_within_at.comp
  (hg : has_mfderiv_within_at g (f '' s) (f x) g') (hf : has_mfderiv_within_at f s x f') :
  has_mfderiv_within_at (g ∘ f) s x (g'.comp f') :=
begin
  refine ⟨continuous_within_at.comp hg.1 hf.1 (subset.refl _), _⟩,
  have A : has_fderiv_within_at ((written_in_ext_chart_at k (f x) g) ∘ (written_in_ext_chart_at k x f))
    (bounded_linear_map.comp g' f')
    ((ext_chart_at k x).inv_fun ⁻¹' s ∩ range (I.to_fun))
    ((ext_chart_at k x).to_fun x),
  { have : (ext_chart_at k x).inv_fun ⁻¹' (f ⁻¹' (ext_chart_at k (f x)).source)
    ∈ nhds_within ((ext_chart_at k x).to_fun x) ((ext_chart_at k x).inv_fun ⁻¹' s ∩ range I.to_fun) :=
      (ext_chart_preimage_mem_nhds_within k x (hf.1.preimage_mem_nhds_within (ext_chart_at_source_mem_nhds _ _))),
    unfold has_mfderiv_within_at at *,
    rw [← has_fderiv_within_at_inter' this, ← ext_chart_preimage_inter_eq] at hf ⊢,
    apply has_fderiv_within_at.comp ((ext_chart_at k x).to_fun x) _ hf.2,
    have : written_in_ext_chart_at k x f ((ext_chart_at k x).to_fun x) = (ext_chart_at k (f x)).to_fun (f x),
      by simp [written_in_ext_chart_at, local_equiv.to_inv, mem_ext_chart_at_source],
    rw this,
    have : (ext_chart_at k (f x)).inv_fun ⁻¹' ((ext_chart_at k (f x)).source)
              ∈ nhds ((ext_chart_at k (f x)).to_fun (f x)) :=
      ext_chart_preimage_mem_nhds _ _ (ext_chart_at_source_mem_nhds _ _),
    rw ← has_fderiv_within_at_inter this,
    apply hg.2.mono,
    rintros y ⟨hy1, hy2⟩,
    rcases (mem_image _ _ _).1 hy1 with ⟨z, ⟨zs, zI⟩, zy⟩,
    rw ← zy,
    unfold written_in_ext_chart_at,
    split,
    { simp only [mem_preimage_eq, function.comp_app],
      rw (ext_chart_at k (f x)).to_inv,
      { exact mem_image_of_mem _ zs.1 },
      { simp [zy.symm, ext_chart_at, written_in_ext_chart_at] at hy2,
        rw local_equiv.to_inv at hy2,
        { exact hy2 },
        { rw ext_chart_at_source at zs,
          exact zs.2 } } },
    { simp only [ext_chart_at, function.comp_app, local_equiv.trans_to_fun,
                 local_equiv.trans_inv_fun, mem_range_self] } },
  apply A.congr' (written_in_ext_chart_comp hf.1),
  -- the next line should be useless, but without it the proof succeeds but the theorem is rejected
  -- TODO: fix
  rw written_in_ext_chart_at,
  simp [written_in_ext_chart_at, ext_chart_at, local_equiv.to_inv, mem_some_chart_at_source]
end

/-- The chain rule. -/
theorem has_mfderiv_at.comp
  (hg : has_mfderiv_at g (f x) g') (hf : has_mfderiv_at f x f') :
  has_mfderiv_at (g ∘ f) x (g'.comp f') :=
begin
  rw ← has_mfderiv_within_at_univ at *,
  exact has_mfderiv_within_at.comp x (hg.mono (subset_univ _)) hf
end

theorem has_mfderiv_at.comp_has_mfderiv_within_at
  (hg : has_mfderiv_at g (f x) g') (hf : has_mfderiv_within_at f s x f') :
  has_mfderiv_within_at (g ∘ f) s x (g'.comp f') :=
begin
  rw ← has_mfderiv_within_at_univ at *,
  exact has_mfderiv_within_at.comp x (hg.mono (subset_univ _)) hf
end

lemma mdifferentiable_within_at.comp
  (hg : mdifferentiable_within_at k g u (f x)) (hf : mdifferentiable_within_at k f s x)
  (h : f '' s ⊆ u) : mdifferentiable_within_at k (g ∘ f) s x :=
begin
  rcases hf.2 with ⟨f', hf'⟩,
  have F : has_mfderiv_within_at f s x f' := ⟨hf.1, hf'⟩,
  rcases hg.2 with ⟨g', hg'⟩,
  have G : has_mfderiv_within_at g u (f x) g' := ⟨hg.1, hg'⟩,
  exact (has_mfderiv_within_at.comp x (G.mono h) F).mdifferentiable_within_at
end

lemma mdifferentiable_at.comp
  (hg : mdifferentiable_at k g (f x)) (hf : mdifferentiable_at k f x) :
  mdifferentiable_at k (g ∘ f) x :=
(hg.has_mfderiv_at.comp x hf.has_mfderiv_at).mdifferentiable_at

lemma mfderiv_within.comp
  (hg : mdifferentiable_within_at k g u (f x)) (hf : mdifferentiable_within_at k f s x)
  (h : f '' s ⊆ u) (hxs : unique_mdiff_within_at k s x) :
  mfderiv_within k (g ∘ f) s x = (mfderiv_within k g u (f x)).comp (mfderiv_within k f s x) :=
begin
  apply has_mfderiv_within_at.mfderiv_within _ hxs,
  apply has_mfderiv_within_at.comp x _ hf.has_mfderiv_within_at,
  apply hg.has_mfderiv_within_at.mono h
end

lemma mfderiv.comp
  (hg : mdifferentiable_at k g (f x)) (hf : mdifferentiable_at k f x) :
  mfderiv k (g ∘ f) x = (mfderiv k g (f x)).comp (mfderiv k f x) :=
begin
  apply has_mfderiv_at.mfderiv,
  exact has_mfderiv_at.comp x hg.has_mfderiv_at hf.has_mfderiv_at
end

lemma mdifferentiable_on.comp
  (hg : mdifferentiable_on k g u) (hf : mdifferentiable_on k f s) (st : f '' s ⊆ u) :
  mdifferentiable_on k (g ∘ f) s :=
λx hx, mdifferentiable_within_at.comp x (hg (f x) (st (mem_image_of_mem _ hx))) (hf x hx) st

lemma mdifferentiable.comp
  (hg : mdifferentiable k g) (hf : mdifferentiable k f) : mdifferentiable k (g ∘ f) :=
λx, mdifferentiable_at.comp x (hg (f x)) (hf x)

end derivatives_properties

#exit

section mfderiv_fderiv

/- The manifold derivative mderiv, when considered on the model vector space with its trivial
manifold structure, coincides with the usual Frechet derivative fderiv. In this section, we prove
this and related statements -/

variables {k : Type} [nondiscrete_normed_field k]
{E : Type} [normed_space k E]
{F : Type} [normed_space k F]
{f : E → F} {x : E} {s : set E}
include E k

lemma unique_mdiff_within_at_iff_unique_diff_within_at :
  unique_mdiff_within_at k s x ↔ unique_diff_within_at k s x :=
by simp [unique_mdiff_within_at]

lemma unique_mdiff_on_iff_unique_diff_on :
  unique_mdiff_on k s ↔ unique_diff_on k s :=
by simp [unique_mdiff_on, unique_diff_on, unique_mdiff_within_at_iff_unique_diff_within_at]

include F

/-- For maps between vector spaces, mdifferentiable_within_at and fdifferentiable_within_at coincide -/
theorem mdifferentiable_within_at_iff_differentiable_within_at :
  mdifferentiable_within_at k f s x ↔ differentiable_within_at k f s x :=
begin
  unfold mdifferentiable_within_at,
  simp {contextual:=tt},
  split,
  { exact λH, by simpa using H (local_homeomorph.refl E) (local_homeomorph.refl F) rfl rfl },
  { assume H e e' he he',
    rw he,
    simpa using H }
end

/-- For maps between vector spaces, mdifferentiable_at and fdifferentiable_at coincide -/
theorem mdifferentiable_at_iff_differentiable_at :
  mdifferentiable_at k f x ↔ differentiable_at k f x :=
begin
  unfold mdifferentiable_at,
  simp {contextual:=tt},
  split,
  { exact λH, by simpa using H (local_homeomorph.refl E) (local_homeomorph.refl F) rfl rfl },
  { assume H e e' he he',
    rw he,
    simpa using H }
end

/-- For maps between vector spaces, mdifferentiable_on and differentiable_on coincide -/
theorem mdifferentiable_on_iff_differentiable_on :
  mdifferentiable_on k f s ↔ differentiable_on k f s :=
by simp [mdifferentiable_on, differentiable_on, mdifferentiable_within_at_iff_differentiable_within_at]

/-- For maps between vector spaces, mdifferentiable and differentiable coincide -/
theorem mdifferentiable_iff_differentiable :
  mdifferentiable k f ↔ differentiable k f :=
by simp [mdifferentiable, differentiable, mdifferentiable_at_iff_differentiable_at]

/-- For maps between vector spaces, mderiv_within and fderiv_within coincide -/
theorem mfderiv_within_eq_fderiv_within :
  mfderiv_within k f s x = fderiv_within k f s x :=
by simp [mfderiv_within]

/-- For maps between vector spaces, mderiv and fderiv coincide -/
theorem mderiv_eq_fderiv :
  mfderiv k f x = fderiv k f x :=
by simp [mfderiv]

end mfderiv_fderiv

section tangent_bundle_structure

/- In this section, we construct the manifold structure on the tangent bundle to a manifold. We
should first build a topology on the tangent bundle, and then check that the canonical charts
are compatible. The topology itself is defined thanks to the canonical charts, so we start
by defining them, first as local equivalences and then, once the topology is defined, as local
homeomorphisms -/

variables (k : Type) [nondiscrete_normed_field k]
{E : Type} [normed_space k E]
{M : Type} [topological_space M] [manifold E M] [manifold.smooth 1 k E M]
include k E M

def tangent_chart.equiv (e : local_homeomorph M E) (h : e ∈ atlas E M) :
  local_equiv (tangent_bundle k M) (E × E) :=
{ to_fun := λp, (e.to_fun p.1, (mfderiv k e.to_fun p.1 : tangent_space_at k p.1 → E) p.2),
  inv_fun := λp, ⟨e.inv_fun p.1,
    (mfderiv k e.inv_fun p.1 : E → tangent_space_at k (e.inv_fun p.1)) p.2⟩,
  source := (tangent_bundle_proj k M) ⁻¹' e.source,
  target := set.prod e.target univ,
  to_map := begin
    rintros ⟨x, v⟩ H,
    change x ∈ e.source at H,
    simp [e.to_map _ H]
  end,
  inv_map := begin
    rintros ⟨x, v⟩ H,
    replace H : x ∈ (e.to_local_equiv).target, by simpa using H,
    exact e.inv_map _ H
  end,
  to_inv := begin
    rintros ⟨x, v⟩ H,
    change x ∈ e.source at H,
    simp only [heq_iff_eq, sigma.mk.inj_iff],
    refine ⟨e.to_inv _ H, _⟩,
    dsimp,
  end,

}


end tangent_bundle_structure



#exit

include E M k

def charts_deriv (x : M) (e e' : subtype (charts_at E x)) : E →L[k] E :=
fderiv k (e.1.symm →ₕ e'.1 : E → E) (e.1 x)

lemma times_cont_diff_charts_comp {e e' : local_homeomorph M E}
  (he : e ∈ atlas E M) (he' : e' ∈ atlas E M) :
  times_cont_diff_on k 1 (e.symm →ₕ e') (e.symm →ₕ e').source :=
(compatible (times_cont_diff_groupoid 1 k E) he he').1

lemma mem_charts_comp_source (x : M) (e e' : subtype (charts_at E x)) :
  e.1 x ∈ (e.1.symm →ₕ e'.1).source :=
begin
  rcases e with ⟨e, e_atlas, xe⟩,
  rcases e' with ⟨e', e'_atlas, xe'⟩,
  let y := e x,
  have eyx : e.inv_fun y = x := e.to_inv x xe,
  rw local_homeomorph.trans_source,
  exact ⟨e.to_map _ xe, by rwa ← eyx at xe'⟩
end

lemma differentiable_charts_comp (x : M) (e e' : subtype (charts_at E x)) :
  differentiable_at k (e.1.symm →ₕ e'.1) (e.1 x) :=
((times_cont_diff_charts_comp e.2.1 e'.2.1).1 (e.1 x) (mem_charts_comp_source x e e')).differentiable_at'
(mem_charts_comp_source x e e') (e.1.symm →ₕ e'.1).open_source

lemma charts_deriv_refl (x : M) (e : subtype (charts_at E x)) :
  charts_deriv x e e = bounded_linear_map.id :=
begin
  let y := e x,
  have y_target : y ∈ e.1.target := e.1.to_map x e.2.2,
  suffices : fderiv k (e.1.symm →ₕ e.1 : E → E) y = fderiv k id y,
    by rwa fderiv_id at this,
  apply differentiable_at.fderiv_congr' differentiable_at_id,
  { apply filter.sets_of_superset _ (mem_nhds_sets e.1.open_target y_target) e.1.inv_to },
  { apply e.1.inv_to _ y_target }
end

lemma charts_deriv_trans (x : M) (e e' e'' : subtype (charts_at E x)) :
  bounded_linear_map.comp (charts_deriv x e' e'') (charts_deriv x e e') = charts_deriv x e e'' :=
begin
  symmetry, calc
  fderiv k (e.1.symm →ₕ e''.1 : E → E) (e.1 x)
  = fderiv k ((e'.1.symm →ₕ e''.1) ∘ (e.1.symm →ₕ e'.1) : E → E) (e.1 x) : begin
    symmetry,
    let s := ((e.1.symm →ₕ e'.1) →ₕ (e'.1.symm →ₕ e''.1)).source,
    have s_open : is_open s := ((e.1.symm →ₕ e'.1) →ₕ (e'.1.symm →ₕ e''.1)).open_source,
    have s_comp : ∀y ∈ s, ((e'.1.symm →ₕ e''.1) ∘ (e.1.symm →ₕ e'.1)) y = (e.1.symm →ₕ e''.1) y,
    { assume y hy,
      change e''.1 (e'.1.inv_fun (e'.1.to_fun (e.1.inv_fun y)))
        = e''.1 (e.1.inv_fun y),
      rw e'.1.to_inv,
      simp [s, local_homeomorph.trans_source] at hy,
      exact hy.1.2 },
    have xs : e.1 x ∈ s,
    { simp only [s, local_homeomorph.trans_source, local_homeomorph.symm_source, mem_preimage_eq,
        local_homeomorph.trans_to_fun, mem_inter_eq, function.comp_app, preimage_inter,
        local_homeomorph.symm_to_fun],
      unfold_coes,
      simp [e.1.to_inv, e'.1.to_inv, e.2.2, e'.2.2, e''.2.2, e.1.to_map, e'.1.to_map] },
    apply differentiable_at.fderiv_congr' (differentiable_charts_comp x e e''),
    { exact filter.sets_of_superset _ (mem_nhds_sets s_open xs) s_comp },
    { exact s_comp _ xs }
  end
  ... = bounded_linear_map.comp (fderiv k (e'.1.symm →ₕ e''.1 : E → E) (e'.1 x))
                                (fderiv k (e.1.symm →ₕ e'.1 : E → E) (e.1 x)) : begin
    have A :  (e.1.symm →ₕ e'.1) (e.1 x) = e'.1 x := calc
      (e.1.symm →ₕ e'.1) (e.1 x) = e'.1 (e.1.inv_fun (e.1.to_fun x)) : rfl
      ... = e'.1 x : by rw e.1.to_inv _ e.2.2,
    have := fderiv.comp (differentiable_charts_comp x e e'),
    rw A at this,
    exact this (differentiable_charts_comp x e' e'')
  end
end

def tangent_vector_equiv_rel (x : M) (p q : tangent_space_unfolded k x) : Prop :=
  (charts_deriv x p.1 q.1) p.2 = q.2

#exit

instance tangent_vector_equiv_rel_setoid (x : M) : setoid (tangent_space_unfolded k x) :=
{ r     := tangent_vector_equiv_rel x,
  iseqv := ⟨begin
    rintros ⟨⟨e, e_atlas, xe⟩, v⟩,
    let y := e x,
    have y_target : y ∈ e.target := e.to_map x xe,
    change (fderiv k (e.symm →ₕ e) y : E → E) v = v,
    suffices : fderiv k (e.symm →ₕ e) y = fderiv k id y,
      by rw [this, fderiv_id, bounded_linear_map.coe_id', id.def],
    apply differentiable_at.fderiv_congr' differentiable_at_id,
    { apply filter.sets_of_superset _ (mem_nhds_sets e.open_target y_target) e.inv_to },
    { apply e.inv_to _ y_target }
  end,
  begin
    rintros ⟨⟨e, e_atlas, xe⟩, v⟩ ⟨⟨e', e'_atlas, xe'⟩, w⟩ h,
    let y := e x,
    have eyx : e.inv_fun y = x := e.to_inv x xe,
    have y_source : y ∈ (e.symm →ₕ e').source,
    { rw local_homeomorph.trans_source,
      exact ⟨e.to_map _ xe, by rwa ← eyx at xe'⟩ },
    let y' := e' x,
    have ey'x : e'.inv_fun y' = x := e'.to_inv x xe',
    have y'y : y' = (e.symm →ₕ e') y,
    { change e' x = e' (e.inv_fun (e.to_fun x)),
      rw e.to_inv x xe },
    have y'_source : y' ∈ (e'.symm →ₕ e).source,
    { rw local_homeomorph.trans_source,
      exact ⟨e'.to_map _ xe', by rwa ← ey'x at xe⟩ },
    change (fderiv k (e.symm →ₕ e') y : E → E) v = w at h,
    change (fderiv k (e'.symm →ₕ e) y' : E → E) w = v,
    rw [← h],
    have : fderiv k ((e'.symm →ₕ e) ∘ (e.symm →ₕ e')) y = fderiv k id y,
    { have ysource2 : y ∈ ((e.symm →ₕ e') →ₕ (e'.symm →ₕ e)).source,
      { rw local_homeomorph.trans_source,
        exact ⟨y_source, by { unfold_coes at y'y, rwa [mem_preimage_eq, ← y'y] }⟩ },
      have : ∀z ∈ ((e.symm →ₕ e') →ₕ (e'.symm →ₕ e)).source, ((e.symm →ₕ e') →ₕ (e'.symm →ₕ e)) z = z,
      { assume z,
        have A : (e.symm →ₕ e') →ₕ (e'.symm →ₕ e) ≈ (local_homeomorph.refl E).restr (e.target) := calc
          (e.symm →ₕ e') →ₕ (e'.symm →ₕ e) ≈ (e.symm →ₕ  (e' →ₕ e'.symm)) →ₕ e : sorry
          ... ≈ (e.symm →ₕ ((local_homeomorph.refl M).restr (e'.source))) →ₕ e : sorry
          ... ≈
        sorry },
      apply differentiable_at_id.fderiv_congr',
      { apply filter.sets_of_superset _
          (mem_nhds_sets ((e.symm →ₕ e') →ₕ (e'.symm →ₕ e)).open_source ysource2) this },
      { apply this _ ysource2 } },
    have Z : (fderiv_at k ((e'.symm →ₕ e) ∘ (e.symm →ₕ e')) y : E → E) v = v,
      by { rw [this, fderiv_at_id], refl },
    rw [fderiv_at.comp, ← y'y] at Z,
    { exact Z },
    { exact ((compat e_atlas e'_atlas).1.1 y y_source).differentiable_at y_source
        (e.symm →ₕ e').open_source },
    { rw ← y'y,
      apply ((compat e'_atlas e_atlas).1.1 y' y'_source).differentiable_at y'_source
        (e'.symm →ₕ e).open_source }
  end

  , sorry⟩ }


end tangent_space