OAI/Analysis/FiniteFactor/OrbitSampling/TrimmedWeak.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceSamplingTrimmedFinite line 11
2. def OAI.FiniteFactor.sourceSamplingTrimmedTorus line 15
3. theorem OAI.FiniteFactor.sourceSampling_discarded_tendsto line 19
4. def OAI.FiniteFactor.finiteMeasureRestrict line 34
5. theorem OAI.FiniteFactor.finiteMeasure_restrict_tendsto line 40

   Source documentation

   A restriction whose discarded mass tends to zero has the same finite weak limit. The norm bound gives the actual error for every test function.

   theorem finiteMeasure_restrict_tendsto {Ω : Type*} [MeasurableSpace Ω]
       [TopologicalSpace Ω] [OpensMeasurableSpace Ω]
       (μ : ℕ → FiniteMeasure Ω) (ν : FiniteMeasure Ω) (A : Set Ω) (hA : MeasurableSet A)
       (hμ : Tendsto μ atTop (𝓝 ν))
       (hloss : Tendsto (fun n => ((μ n : Measure Ω) Aᶜ).toReal) atTop (𝓝 0)) :
       Tendsto (fun n => finiteMeasureRestrict (μ n) A)
         atTop (𝓝 ν) := by
   …

   Mentions: OAI.FiniteFactor.finiteMeasureRestrict

6. theorem OAI.FiniteFactor.sourceSamplingTrimmed_weak_event line 68

   Source documentation

   Actual ordered measures have the same compact-torus weak limit, for all continuous tests, on one probability-one angle event.

   theorem sourceSamplingTrimmed_weak_event : ∀ᵐ θ ∂sourceAngleLaw,
       ∀ I : Finset SourceCoordinate,
         Tendsto (fun s => sourceSamplingTrimmedFinite I s θ) atTop (𝓝 (sourceSamplingLambdaFinite I)) ∧
         Tendsto (fun s => sourceSamplingTrimmedTorus I s θ) atTop (𝓝 (sourceSamplingLambdaTorus I)) ∧
         ∀ f : C(SourceSamplingTorus,ℝ),
           Tendsto (fun s => ∫ p, f p ∂(sourceSamplingTrimmedTorus I s θ : Measure SourceSamplingTorus))
             atTop (𝓝 (∫ p, f p ∂(sourceSamplingLambdaTorus I : Measure SourceSamplingTorus))) := by
   …

   Mentions: OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingTrimmedFinite, OAI.FiniteFactor.sourceSamplingLambdaFinite, OAI.FiniteFactor.sourceSamplingTrimmedTorus, OAI.FiniteFactor.sourceSamplingLambdaTorus, OAI.FiniteFactor.SourceSamplingTorus