OAI/Analysis/FiniteFactor/OrbitSampling/DiagonalIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceSampling_diagonal_integral_tendsto line 12

   Source documentation

   The actual one-coordinate diagonal model converges to uniform diagonal mass on every measurable first test and closed-interval second test.

   theorem sourceSampling_diagonal_integral_tendsto (E : Set ℝ) (hE : MeasurableSet E) (a c : ℝ) :
       Tendsto (fun stage => ∫ s,
         samplingTestedFirstDensity false (sourceSamplingWidth stage) (sourceSamplingCutoff stage)
           E (Set.Icc a c) s ∂unitIntervalMeasure)
         atTop (𝓝 ((unitIntervalMeasure (E ∩ Set.Icc a c)).toReal)) := by
   …

   Mentions: OAI.FiniteFactor.samplingTestedFirstDensity, OAI.FiniteFactor.sourceSamplingWidth, OAI.FiniteFactor.sourceSamplingCutoff, OAI.FiniteFactor.unitIntervalMeasure

2. theorem OAI.FiniteFactor.samplingTestedFirstDensity_triangular_parameters line 51

   Source documentation

   Triangular tested factors are independent of the sampling width and cutoff.

   theorem samplingTestedFirstDensity_triangular_parameters (h α h' α' s : ℝ) (E G : Set ℝ) :
       samplingTestedFirstDensity true h α E G s = samplingTestedFirstDensity true h' α' E G s := by
   …

   Mentions: OAI.FiniteFactor.samplingTestedFirstDensity