OAI/GroupTheory/PolycyclicRecognition/Analysis/SupportedProfileConstraints.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.integral_tendsto_of_uniformly_and_weakly line 17

   Source documentation

   Uniformly convergent observables can be integrated against a weakly convergent family of probabilities. Both vary in this statement.

   theorem integral_tendsto_of_uniformly_and_weakly
       {X ι : Type*} [TopologicalSpace X] [CompactSpace X]
       [MeasurableSpace X] [BorelSpace X] {l : Filter ι}
       (μs : ι → ProbabilityMeasure X) (μ : ProbabilityMeasure X)
       (hμ : Tendsto μs l (𝓝 μ)) (fs : ι → C(X, ℝ)) (f : C(X, ℝ))
       (hf : TendstoUniformly (fun i x => fs i x) f l) :
       Tendsto (fun i => ∫ x, fs i x ∂(μs i : Measure X)) l
         (𝓝 (∫ x, f x ∂(μ : Measure X))) := by
   …

2. theorem OAI.PolycyclicRecognition.zero_on_support_of_uniformly_vanishing_integrals line 46

   Source documentation

   A continuous nonnegative error with vanishing expectations vanishes at every point in the support of the weak limit.

   theorem zero_on_support_of_uniformly_vanishing_integrals
       {X ι : Type*} [TopologicalSpace X] [CompactSpace X]
       [MeasurableSpace X] [BorelSpace X] {l : Filter ι} [l.NeBot]
       (μs : ι → ProbabilityMeasure X) (μ : ProbabilityMeasure X)
       (hμ : Tendsto μs l (𝓝 μ)) (fs : ι → C(X, ℝ)) (f : C(X, ℝ))
       (hf : TendstoUniformly (fun i x => fs i x) f l)
       (hpos : ∀ x, 0 ≤ f x)
       (hzero : Tendsto (fun i => ∫ x, fs i x ∂(μs i : Measure X)) l (𝓝 0))
       {x : X} (hx : x ∈ (μ : Measure X).support) : f x = 0 := by
   …

3. theorem OAI.PolycyclicRecognition.mem_on_support_of_uniformly_vanishing_distance line 65

   Source documentation

   Apply the preceding result to distance from a nonempty closed convex constraint set. The conclusion holds on the support, not just almost surely.

   theorem mem_on_support_of_uniformly_vanishing_distance
       {X W ι : Type*} [TopologicalSpace X] [CompactSpace X]
       [MeasurableSpace X] [BorelSpace X] [PseudoMetricSpace W]
       {l : Filter ι} [l.NeBot]
       (μs : ι → ProbabilityMeasure X) (μ : ProbabilityMeasure X)
       (hμ : Tendsto μs l (𝓝 μ)) (vs : ι → C(X, W)) (v : C(X, W))
       (hv : TendstoUniformly (fun i x => vs i x) v l)
       {S : Set W} (hS : IsClosed S) (hne : S.Nonempty)
       (hzero : Tendsto (fun i => ∫ x, infDist (vs i x) S ∂(μs i : Measure X)) l (𝓝 0))
       {x : X} (hx : x ∈ (μ : Measure X).support) : v x ∈ S := by
   …