OAI/Analysis/FiniteFactor/OrbitSampling/DiagonalEvent.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sampling_ae_summable_of_integrals line 13

   Source documentation

   Tonelli converts summable expectations of nonnegative functions into pointwise summability on a conull event.

   theorem sampling_ae_summable_of_integrals {Ω : Type*} [MeasurableSpace Ω]
       (μ : Measure Ω) (f : ℕ → Ω → ℝ) (hm : ∀ n, Measurable (f n))
       (hi : ∀ n, Integrable (f n) μ) (hn : ∀ n x, 0 ≤ f n x)
       (hs : Summable (fun n => ∫ x, f n x ∂μ)) :
       ∀ᵐ x ∂μ, Summable (fun n => f n x) := by
   …

2. theorem OAI.FiniteFactor.sourceSamplingDiagonalContribution_measurable line 29
3. theorem OAI.FiniteFactor.sourceSamplingDiagonalContribution_ae line 39

   Source documentation

   A genuine conull conclusion for the actual diagonal contribution. This does not assert convergence of the full empirical sampling error.

   theorem sourceSamplingDiagonalContribution_ae (r : Bool) (b : SourceCoordinate → Bool)
       (E G : SourceCoordinate → Set ℝ) (hE : ∀ i, MeasurableSet (E i)) (hG : ∀ i, MeasurableSet (G i)) :
       ∀ᵐ θ ∂sourceAngleLaw,
         Summable (fun stage => sourceSamplingDiagonalContribution stage r b E G θ) ∧
         Tendsto (fun stage => sourceSamplingDiagonalContribution stage r b E G θ) atTop (𝓝 0) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.sourceSamplingDiagonalContribution

4. theorem OAI.FiniteFactor.sourceSamplingDiagonalContribution_countable_event line 54

   Source documentation

   One conull event handles every member of any countable family of source tests, orientations and triangular-coordinate choices for the diagonal term.

   theorem sourceSamplingDiagonalContribution_countable_event {ι : Type*} [Countable ι]
       (r : ι → Bool) (b : ι → SourceCoordinate → Bool) (E G : ι → SourceCoordinate → Set ℝ)
       (hE : ∀ j i, MeasurableSet (E j i)) (hG : ∀ j i, MeasurableSet (G j i)) :
       ∀ᵐ θ ∂sourceAngleLaw, ∀ j,
         Summable (fun stage => sourceSamplingDiagonalContribution stage (r j) (b j) (E j) (G j) θ) ∧
         Tendsto (fun stage => sourceSamplingDiagonalContribution stage (r j) (b j) (E j) (G j) θ) atTop (𝓝 0) :=
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.sourceSamplingDiagonalContribution