OAI/GroupTheory/PolycyclicRecognition/Geometry/FlowProbabilityCutoffs.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_flow_probability_cutoffs line 19

   Source documentation

   A segment in the open chart admits one starting density and one occupation density. The domination constant works for every time on the segment and all sufficiently late scaled flows, before choosing a mesh.

   theorem exists_flow_probability_cutoffs
       {X ι : Type*} [MetricSpace X] [LocallyCompactSpace X]
       [MeasurableSpace X] [BorelSpace X]
       (m : Measure X) [m.IsOpenPosMeasure] [IsFiniteMeasureOnCompacts m]
       {l : Filter ι} (Fs : ι → C(X × ℝ, X)) (F : C(X × ℝ, X))
       (hF : Tendsto Fs l (𝓝 F)) (z : X) {T : ℝ} (hT : 0 ≤ T)
       {U : Set X} (hU : IsOpen U) (hseg : ∀ t ∈ Icc 0 T, F (z, t) ∈ U) :
       ∃ (η ρ : C(X, ℝ)) (c : ℝ≥0),
         HasCompactSupport η ∧ HasCompactSupport ρ ∧ tsupport ρ ⊆ U ∧
         (∀ x, 0 ≤ η x) ∧ (∀ x, 0 ≤ ρ x) ∧ 0 < η z ∧
         Integrable η m ∧ Integrable ρ m ∧
         (∫ x, η x ∂m) = 1 ∧ (∫ x, ρ x ∂m) = 1 ∧
   …