OAI/Analysis/FiniteFactor/OrbitSampling/Error.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceSamplingEmpiricalDensity line 11
2. def OAI.FiniteFactor.sourceSamplingSquaredError line 17

   Source documentation

   The full sampling error, including every distinct-pair and mixed term.

   def sourceSamplingSquaredError (stage : ℕ) (r : Bool) (b : SourceCoordinate → Bool)
       (E G : SourceCoordinate → Set ℝ) (θ : SourceCoordinate → ℝ) : ℝ :=
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate

3. theorem OAI.FiniteFactor.sourceSampling_error_joint_integrable line 22
4. theorem OAI.FiniteFactor.sourceSamplingSquaredError_integrable line 41
5. theorem OAI.FiniteFactor.sourceSamplingSquaredError_measurable line 46
6. theorem OAI.FiniteFactor.sourceSamplingSquaredError_nonneg line 54
7. theorem OAI.FiniteFactor.sourceSamplingSquaredError_expectation line 60

   Source documentation

   Full expected squared sampling error with the source's actual sample set, weights and ideal density. All distinct-pair and mixed assumptions are proved.

   theorem sourceSamplingSquaredError_expectation (stage : ℕ) (hs : 200000 ≤ sourceBlockSize stage)
       (r : Bool) (b : SourceCoordinate → Bool) (a c a' c' : SourceCoordinate → ℝ) :
       (∫ θ, sourceSamplingSquaredError stage r b (fun i => Set.Icc (a i) (c i)) (fun i => Set.Icc (a' i) (c' i)) θ ∂sourceAngleLaw) ≤
         (∫ θ, sourceSamplingDiagonalContribution stage r b (fun i => Set.Icc (a i) (c i)) (fun i => Set.Icc (a' i) (c' i)) θ ∂sourceAngleLaw)+
         3*sourceSamplingCorrelationBudget stage := by
   …

   Mentions: OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingSquaredError, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.sourceSamplingDiagonalContribution, OAI.FiniteFactor.sourceSamplingCorrelationBudget