OAI/Geometry/Arnold/Homotopy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArnoldCounterexample.Forms.spatial line 22

   Source documentation

   Spatial inclusion in the cylinder.

   def spatial : E →L[ℝ] ℝ × E := (0 : E →L[ℝ] ℝ).prod (.id ℝ E)

2. lemma OAI.ArnoldCounterexample.Forms.spatial_apply line 24
3. def OAI.ArnoldCounterexample.Forms.cylinderContraction line 27

   Source documentation

   Fixed-direction contraction and slice restriction, bundled in norm topology.

   def cylinderContraction (n : ℕ) :
       ((ℝ × E) [⋀^Fin (n + 1)]→L[ℝ] ℝ) →L[ℝ] (E [⋀^Fin n]→L[ℝ] ℝ) :=
   …

4. lemma OAI.ArnoldCounterexample.Forms.cylinderContraction_apply line 38
5. def OAI.ArnoldCounterexample.Forms.sliceContraction line 42
6. lemma OAI.ArnoldCounterexample.Forms.sliceContraction_contDiff line 46
7. theorem OAI.ArnoldCounterexample.Forms.cylinder_homotopy_identity line 53

   Source documentation

   The time derivative of a closed form restricted to slices is the spatial exterior derivative of its contraction with the time direction.

   theorem cylinder_homotopy_identity {n : ℕ}
       (Θ : ℝ × E → (ℝ × E) [⋀^Fin (n + 1)]→L[ℝ] ℝ)
       (hΘ : Differentiable ℝ Θ) (t : ℝ) (z : E)
       (hclosed : extDeriv Θ (t, z) = 0) (v : Fin (n + 1) → E) :
       extDeriv (sliceContraction Θ t) z v =
         (fderiv ℝ Θ (t, z) (1, 0)) (fun i ↦ (0, v i)) := by
   …

   Mentions: OAI.ArnoldCounterexample.Forms.sliceContraction

8. instance OAI.ArnoldCounterexample.Forms.finiteDimensional_multilinear_fin line 90
9. lemma OAI.ArnoldCounterexample.Forms.contDiff_of_toMultilinear line 101

   Source documentation

   Smoothness into finite-dimensional alternating forms can be checked after forgetting alternation. This uses an honest linear retraction, not an axiom.

   lemma contDiff_of_toMultilinear {D : Type uD} [NormedAddCommGroup D] [NormedSpace ℝ D]
       [FiniteDimensional ℝ E] {n : ℕ} {k : ℕ∞ω}
       {f : D → E [⋀^Fin n]→L[ℝ] ℝ}
       (hf : ContDiff ℝ k (fun x ↦ (f x).toContinuousMultilinearMap)) : ContDiff ℝ k f := by
   …

10. lemma OAI.ArnoldCounterexample.Forms.contDiff_pullback_form line 114
11. lemma OAI.ArnoldCounterexample.Forms.pullback_constant_closed line 141

    Source documentation

    Pullback of a constant form is closed.

    lemma pullback_constant_closed {D : Type uD} {F : Type uF}
        [NormedAddCommGroup D] [NormedSpace ℝ D]
        [NormedAddCommGroup F] [NormedSpace ℝ F]
        {n : ℕ} (θ : F [⋀^Fin n]→L[ℝ] ℝ) (H : D → F)
        (hH : ContDiff ℝ ∞ H) (x : D) :
        extDeriv (fun y ↦ θ.compContinuousLinearMap (fderiv ℝ H y)) x = 0 := by
    …