OccupationTranslation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Passing coordinate translation estimates to sampled probabilities

theorem OAI.PolycyclicRecognition.density_product_occupation_error_tendsto_zero line 19

Source documentation

Translation in the density-sampled factor changes the law by a vanishing amount. The other independent factor can vary through the observable and requires no uniformity in its sample points.

theorem density_product_occupation_error_tendsto_zero
    {A D X G ι : Type*} [MeasurableSpace A]
    [TopologicalSpace D] [MeasurableSpace D] [BorelSpace D]
    [TopologicalSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X]
    [SMul G X] [ContinuousConstSMul G X]
    (μ : ProbabilityMeasure A) (m : Measure D) [SFinite m]
    (ρ : D → ℝ) (hc : Continuous ρ) (hi : Integrable ρ m)
    (hp : ∀ z, 0 ≤ ρ z) (hmass : ∫ z, ρ z ∂m = 1)
    {l : Filter ι} [l.IsCountablyGenerated]
    (T : ι → D ≃ᵐ D) (hT : ∀ i, MeasurePreserving (T i) m m)
    (hlim : ∀ z, Tendsto (fun i => (T i).symm z) l (𝓝 z))
    (p : ι → A × D → X) (hmeas : ∀ i, Measurable (p i))
…

theorem OAI.PolycyclicRecognition.first_factor_product_occupation_error_tendsto_zero line 63

Source documentation

A uniform first-factor error remains small after independent sampling of the other coordinate, and is exactly the translated-law error.

theorem first_factor_product_occupation_error_tendsto_zero
    {A D X G ι : Type*} [MeasurableSpace A] [MeasurableSpace D]
    [TopologicalSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X]
    [SMul G X] [ContinuousConstSMul G X]
    (μ : ProbabilityMeasure A) (ν : ProbabilityMeasure D)
    {l : Filter ι} (p : ι → A × D → X) (hmeas : ∀ i, Measurable (p i))
    (U : ι → D → A → A) (g : G)
    (hmove : ∀ i a d, g • p i (a, d) = p i (U i d a, d))
    (f : C(X, ℝ))
    (herror : TendstoUniformly (fun i d =>
      (∫ a, f (p i (U i d a, d)) ∂(μ : Measure A)) -
      ∫ a, f (p i (a, d)) ∂(μ : Measure A)) (fun _ => 0) l) :
…