ProfileRegularity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

From regularity and finite derivative labels to an affine profile

A continuous derivative taking only finitely many values is constant on a connected domain, and the profile is globally affine.

theorem OAI.PolycyclicRecognition.eq_of_continuous_finite_range line 18

Source documentation

A continuous map from a connected space into a finite subset is constant.

theorem eq_of_continuous_finite_range
    {X Y : Type*} [TopologicalSpace X] [PreconnectedSpace X]
    [TopologicalSpace Y] [T1Space Y]
    (f : X → Y) (hf : Continuous f) (hfinite : Set.Finite (Set.range f)) (x y : X) :
    f x = f y := by
…

theorem OAI.PolycyclicRecognition.affine_of_continuous_finite_derivative line 28

Source documentation

A regular profile whose derivatives lie in a finite set has one global linear label. The offset is its value at the identity of the vector space.

theorem affine_of_continuous_finite_derivative
    {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    (f : E → F) (A : E → E →L[ℝ] F)
    (hderiv : ∀ x, HasFDerivAt f (A x) x)
    (hcontinuous : Continuous A) (hfinite : Set.Finite (Set.range A)) :
    ∀ x, f x = f 0 + A 0 x := by
…

theorem OAI.PolycyclicRecognition.mem_closed_of_continuous_ae line 50

Source documentation

For a measure positive on open sets, a continuous map lying in a closed set almost everywhere lies there everywhere.

theorem mem_closed_of_continuous_ae
    {X Y : Type*} [TopologicalSpace X] [MeasurableSpace X]
    [TopologicalSpace Y] [T2Space Y]
    (μ : MeasureTheory.Measure X) [MeasureTheory.Measure.IsOpenPosMeasure μ]
    (f : X → Y) (hf : Continuous f) (S : Set Y) (hS : IsClosed S)
    (hae : ∀ᵐ x ∂μ, f x ∈ S) : ∀ x, f x ∈ S := by
…

theorem OAI.PolycyclicRecognition.affine_of_contDiff_ae_finite_derivative line 66

Source documentation

The almost-everywhere finite-label condition obtained by profile volume comparison suffices after regularity has supplied a continuous derivative.

theorem affine_of_contDiff_ae_finite_derivative
    {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    (μ : MeasureTheory.Measure E) [MeasureTheory.Measure.IsOpenPosMeasure μ]
    (f : E → F) (hf : ContDiff ℝ 1 f)
    (S : Set (E →L[ℝ] F)) (hS : S.Finite)
    (hae : ∀ᵐ x ∂μ, fderiv ℝ f x ∈ S) :
    ∀ x, f x = f 0 + fderiv ℝ f 0 x := by
…