OAI/Geometry/Arnold/Haar.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArnoldCounterexample.CriticalBound.hasDerivAt_integral_of_compact line 18

   Source documentation

   Compactness supplies the uniform domination needed to differentiate a parameter integral. This gives differentiation under the Haar integral.

   theorem hasDerivAt_integral_of_compact
       {G : Type uG} [TopologicalSpace G] [CompactSpace G]
       [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [IsFiniteMeasure μ]
       {F F' : ℝ → G → ℝ}
       (hF : Continuous (Function.uncurry F))
       (hF' : Continuous (Function.uncurry F'))
       (hd : ∀ t g, HasDerivAt (fun s ↦ F s g) (F' t g) t) (t : ℝ) :
       HasDerivAt (fun s ↦ ∫ g, F s g ∂μ) (∫ g, F' t g ∂μ) t := by
   …

2. theorem OAI.ArnoldCounterexample.CriticalBound.integral_derivative_right_translate_eq_zero line 42

   Source documentation

   The integral of a smooth infinitesimal right-translation is zero. Unlike a manifold Stokes interface, this is proved directly from Haar invariance and differentiation under a finite integral.

   theorem integral_derivative_right_translate_eq_zero
       {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
       [MeasurableSpace G] [BorelSpace G] (μ : Measure G)
       [IsFiniteMeasure μ] [μ.IsMulRightInvariant]
       (c : ℝ → G) (hc : Continuous c) (f : G → ℝ) (hf : Continuous f)
       (D : ℝ → G → ℝ) (hD : Continuous (Function.uncurry D))
       (hd : ∀ t g, HasDerivAt (fun s ↦ f (g * c s)) (D t g) t) (t : ℝ) :
       ∫ g, D t g ∂μ = 0 := by
   …

3. abbrev OAI.ArnoldCounterexample.CriticalBound.RM line 63
4. abbrev OAI.ArnoldCounterexample.CriticalBound.O5 line 64
5. lemma OAI.ArnoldCounterexample.CriticalBound.orthogonal_row_sq line 66
6. lemma OAI.ArnoldCounterexample.CriticalBound.orthogonal_entry_abs_le_one line 70
7. theorem OAI.ArnoldCounterexample.CriticalBound.isCompact_orthogonalGroup line 78

   Source documentation

   The actual real orthogonal matrix group is compact; no compact Lie-group or integration-on-manifolds library is being assumed.

   theorem isCompact_orthogonalGroup : IsCompact (Matrix.orthogonalGroup (Fin 5) ℝ : Set RM) := by
   …

   Mentions: OAI.ArnoldCounterexample.CriticalBound.RM

8. instance OAI.ArnoldCounterexample.CriticalBound.o5_compactSpace line 88
9. instance OAI.ArnoldCounterexample.CriticalBound.o5_measurableSpace line 91
10. instance OAI.ArnoldCounterexample.CriticalBound.o5_borelSpace line 92
11. def OAI.ArnoldCounterexample.CriticalBound.haar line 94
12. example OAI.ArnoldCounterexample.CriticalBound.(example at line 96) line 96
13. example OAI.ArnoldCounterexample.CriticalBound.(example at line 97) line 97
14. example OAI.ArnoldCounterexample.CriticalBound.(example at line 98) line 98
15. instance OAI.ArnoldCounterexample.CriticalBound.haar_finite line 111
16. instance OAI.ArnoldCounterexample.CriticalBound.haar_rightInvariant line 112
17. instance OAI.ArnoldCounterexample.CriticalBound.haar_openPos line 113
18. def OAI.ArnoldCounterexample.CriticalBound.expCurve line 116

    Source documentation

    The actual one-parameter subgroup generated by a skew real matrix.

    def expCurve (X : RM) (hX : star X = -X) (t : ℝ) : O5 :=
    …

    Mentions: OAI.ArnoldCounterexample.CriticalBound.RM, OAI.ArnoldCounterexample.CriticalBound.O5

19. lemma OAI.ArnoldCounterexample.CriticalBound.expCurve_continuous line 120
20. lemma OAI.ArnoldCounterexample.CriticalBound.right_expCurve_hasDerivAt line 123
21. theorem OAI.ArnoldCounterexample.CriticalBound.integral_fderiv_mul_skew_eq_zero line 131

    Source documentation

    Integration kills every left-invariant directional derivative of a C1 ambient function on this compact orthogonal group.

    theorem integral_fderiv_mul_skew_eq_zero (f : RM → ℝ) (hf : ContDiff ℝ ∞ f)
        (X : RM) (hX : star X = -X) :
        ∫ A : O5, fderiv ℝ f (A : RM) ((A : RM) * X) ∂haar = 0 := by
    …

    Mentions: OAI.ArnoldCounterexample.CriticalBound.RM, OAI.ArnoldCounterexample.CriticalBound.O5, OAI.ArnoldCounterexample.CriticalBound.haar