OAI/Analysis/FiniteFactor/OrbitSampling/ProductError.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceSamplingCorrelationBudget line 10
2. theorem OAI.FiniteFactor.sourceSampling_coordinate_product_error line 14

   Source documentation

   Uniform telescoping budget from the actual ideal coordinate moments.

   theorem sourceSampling_coordinate_product_error (stage : ℕ) (r : Bool) (b : SourceCoordinate → Bool)
       (E G : SourceCoordinate → Set ℝ) (hE : ∀ i, MeasurableSet (E i)) (hG : ∀ i, MeasurableSet (G i))
       (f : SourceCoordinate → ℝ) (hf : ∀ i ∈ sourceSamplingPrefix stage, 0 ≤ f i)
       (he : ∀ i ∈ sourceSamplingPrefix stage,
         |f i-(∫ s, samplingOrientedDensity r (b i) (sourceSamplingWidth stage) (sourceSamplingCutoff stage)
           (E i) (G i) s^2 ∂unitIntervalMeasure)| ≤ 104*(sourceBlockSize stage : ℝ)^(-74 : ℝ)) :
       |(∏ i ∈ sourceSamplingPrefix stage, f i)-
         (∫ x, sourceSamplingIdealDensity stage r b E G x^2
           ∂Measure.infinitePi (fun _ : SourceCoordinate => unitIntervalMeasure))| ≤ sourceSamplingCorrelationBudget stage := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingPrefix, OAI.FiniteFactor.samplingOrientedDensity, OAI.FiniteFactor.sourceSamplingWidth, OAI.FiniteFactor.sourceSamplingCutoff, OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.sourceSamplingIdealDensity, OAI.FiniteFactor.sourceSamplingCorrelationBudget

3. theorem OAI.FiniteFactor.sourceSamplingProduct_pair_error line 62

   Source documentation

   Distinct products under the actual angle and Haar laws.

   theorem sourceSamplingProduct_pair_error (stage : ℕ) (hs : 200000 ≤ sourceBlockSize stage)
       (r : Bool) (b : SourceCoordinate → Bool) (a c a' c' : SourceCoordinate → ℝ)
       (n k : ℤ) (hn : n ∈ sourceSamplingPowers stage) (hk : k ∈ sourceSamplingPowers stage) (hne : n ≠ k) :
       |(∫ θ, ∫ x, sourceSamplingProduct stage r b (fun i => Set.Icc (a i) (c i)) (fun i => Set.Icc (a' i) (c' i)) n θ x *
           sourceSamplingProduct stage r b (fun i => Set.Icc (a i) (c i)) (fun i => Set.Icc (a' i) (c' i)) k θ x
           ∂Measure.infinitePi (fun _ : SourceCoordinate => unitIntervalMeasure) ∂sourceAngleLaw)-
         (∫ x, sourceSamplingIdealDensity 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))| ≤ sourceSamplingCorrelationBudget stage := by
   …

   Mentions: OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingPowers, OAI.FiniteFactor.sourceSamplingProduct, OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.sourceSamplingIdealDensity, OAI.FiniteFactor.sourceSamplingCorrelationBudget

4. theorem OAI.FiniteFactor.sourceSamplingProduct_mixed_error line 86

   Source documentation

   Actual mixed products have the same uniform error budget.

   theorem sourceSamplingProduct_mixed_error (stage : ℕ) (hs : 200000 ≤ sourceBlockSize stage)
       (r : Bool) (b : SourceCoordinate → Bool) (E G : SourceCoordinate → Set ℝ)
       (hE : ∀ i, MeasurableSet (E i)) (hG : ∀ i, MeasurableSet (G i))
       (n : ℤ) (hn : n ∈ sourceSamplingPowers stage) :
       |(∫ θ, ∫ x, sourceSamplingProduct stage r b E G n θ x*sourceSamplingIdealDensity stage r b E G x
           ∂Measure.infinitePi (fun _ : SourceCoordinate => unitIntervalMeasure) ∂sourceAngleLaw)-
         (∫ x, sourceSamplingIdealDensity stage r b E G x^2
           ∂Measure.infinitePi (fun _ : SourceCoordinate => unitIntervalMeasure))| ≤ sourceSamplingCorrelationBudget stage := by
   …

   Mentions: OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingPowers, OAI.FiniteFactor.sourceSamplingProduct, OAI.FiniteFactor.sourceSamplingIdealDensity, OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.sourceSamplingCorrelationBudget