SingleCorrelation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceSampling_single_phase_budget line 12
Source documentation
The source powers make the single-phase relative error at most m^-80.
```
theorem sourceSampling_single_phase_budget (stage : ℕ) (hs : 200000 ≤ sourceBlockSize stage)
    (i : SourceCoordinate) (hi : i.1 ≤ stage) (n : ℤ) (hn : n ∈ sourceSamplingPowers stage) :
    1/((n : ℝ)*sourceAngleUnit i) ≤ (sourceBlockSize stage : ℝ)^(-80 : ℝ) := by
…
```
Mentions: OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingPowers, OAI.FiniteFactor.sourceAngleUnit

theorem OAI.FiniteFactor.sourceSampling_single_phase_relative line 48

Source documentation

Actual full-angle single-phase test, with all source sampling hypotheses.

theorem sourceSampling_single_phase_relative (stage : ℕ) (hs : 200000 ≤ sourceBlockSize stage)
    (i : SourceCoordinate) (hi : i.1 ≤ stage) (n : ℤ) (hn : n ∈ sourceSamplingPowers stage)
    (g : ℝ → ℝ) (hg : ∀ t, 0 ≤ g t) (hgm : Measurable g) (hgi : Integrable g unitIntervalMeasure) :
    |(∫ θ, g (Int.fract ((n : ℝ)*θ i)) ∂sourceAngleLaw)-(∫ t, g t ∂unitIntervalMeasure)| ≤
      (sourceBlockSize stage : ℝ)^(-80 : ℝ)*(∫ t, g t ∂unitIntervalMeasure) := by
…

Mentions: OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingPowers, OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.sourceAngleLaw

theorem OAI.FiniteFactor.sourceSampling_coordinate_mixed_error line 62

Source documentation

The actual mixed q_n/Z_l^0 coordinate factor, for every orientation and all measurable tests, has error at most 5*m^-80.

theorem sourceSampling_coordinate_mixed_error (stage : ℕ) (hs : 200000 ≤ sourceBlockSize stage)
    (i : SourceCoordinate) (hi : i.1 ≤ stage) (n : ℤ) (hn : n ∈ sourceSamplingPowers stage)
    (r b : Bool) (E G : Set ℝ) (hE : MeasurableSet E) (hG : MeasurableSet G) :
    |(∫ s, samplingOrientedDensity r b (sourceSamplingWidth stage) (sourceSamplingCutoff stage) E G s *
        (∫ θ, samplingOrientedWeight r b (sourceSamplingWidth stage) (sourceSamplingCutoff stage)
          E G s (Int.fract ((n : ℝ)*θ i)) ∂sourceAngleLaw) ∂unitIntervalMeasure)-
      (∫ s, samplingOrientedDensity r b (sourceSamplingWidth stage) (sourceSamplingCutoff stage) E G s^2 ∂unitIntervalMeasure)| ≤
      5*(sourceBlockSize stage : ℝ)^(-80 : ℝ) := by
…

Mentions: OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingPowers, OAI.FiniteFactor.samplingOrientedDensity, OAI.FiniteFactor.sourceSamplingWidth, OAI.FiniteFactor.sourceSamplingCutoff, OAI.FiniteFactor.samplingOrientedWeight, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.unitIntervalMeasure