OAI/Analysis/FiniteFactor/OrbitSampling/UniformEvent.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceSamplingEmpiricalDensity_uniform line 11

   Source documentation

   Actual empirical L2 bounds, uniform over all stages on a conull event.

   theorem sourceSamplingEmpiricalDensity_uniform (r : Bool) (b : SourceCoordinate → Bool)
       (a c a' c' : SourceCoordinate → ℝ) :
       ∀ᵐ θ ∂sourceAngleLaw, ∃ C : ℝ, ∀ stage,
         MemLp (sourceSamplingEmpiricalDensity stage r b
           (fun i => Set.Icc (a i) (c i)) (fun i => Set.Icc (a' i) (c' i)) θ) 2
             (Measure.infinitePi (fun _ : SourceCoordinate => unitIntervalMeasure)) ∧
         (∫ x, sourceSamplingEmpiricalDensity stage r b
           (fun i => Set.Icc (a i) (c i)) (fun i => Set.Icc (a' i) (c' i)) θ x^2
           ∂Measure.infinitePi (fun _ : SourceCoordinate => unitIntervalMeasure)) ≤ C := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.sourceSamplingEmpiricalDensity, OAI.FiniteFactor.unitIntervalMeasure

2. theorem OAI.FiniteFactor.sourceSampling_full_L2_event line 35

   Source documentation

   A single event gives full sampling convergence and uniform empirical L2 bounds for every member of any countable source test family.

   theorem sourceSampling_full_L2_event {ι : Type*} [Countable ι]
       (r : ι → Bool) (b : ι → SourceCoordinate → Bool)
       (a c a' c' : ι → SourceCoordinate → ℝ) :
       ∀ᵐ θ ∂sourceAngleLaw, ∀ j,
         Tendsto (fun stage => sourceSamplingSquaredError stage (r j) (b j)
           (fun i => Set.Icc (a j i) (c j i)) (fun i => Set.Icc (a' j i) (c' j i)) θ) atTop (𝓝 0) ∧
         ∃ C : ℝ, ∀ stage,
           MemLp (sourceSamplingEmpiricalDensity stage (r j) (b j)
             (fun i => Set.Icc (a j i) (c j i)) (fun i => Set.Icc (a' j i) (c' j i)) θ) 2
               (Measure.infinitePi (fun _ : SourceCoordinate => unitIntervalMeasure)) ∧
           (∫ x, sourceSamplingEmpiricalDensity stage (r j) (b j)
             (fun i => Set.Icc (a j i) (c j i)) (fun i => Set.Icc (a' j i) (c' j i)) θ x^2
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.sourceSamplingSquaredError, OAI.FiniteFactor.sourceSamplingEmpiricalDensity, OAI.FiniteFactor.unitIntervalMeasure