OAI/GroupTheory/PolycyclicRecognition/Analysis/LipschitzProfileFTC.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.scalar_lipschitz_fundamental_identity line 16
2. theorem OAI.PolycyclicRecognition.profile_weight_fundamental_identities line 40
3. theorem OAI.PolycyclicRecognition.affine_of_lipschitz_ae_constant_derivative line 55

   Source documentation

   The spanning weights detect an affine vector-valued line when its almost-everywhere derivative is constant.

   theorem affine_of_lipschitz_ae_constant_derivative
       {W I : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
       (α : I → W →L[ℝ] ℝ) (hsep : ∀ w : W, (∀ i, α i w = 0) → w = 0)
       {h : ℝ → W} {C : ℝ≥0} {T : ℝ} (hT : 0 ≤ T)
       (hh : LipschitzOnWith C h (Icc 0 T)) (u : W)
       (hderiv : ∀ᵐ t ∂volume.restrict (Icc 0 T), HasDerivAt h u t) :
       ∀ t ∈ Icc 0 T, h t = h 0 + t • u := by
   …