SecondCorrelation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceSampling_max_height line 12
Source documentation
Uniform source height bound, for either marginal orientation.
```
theorem sourceSampling_max_height (stage : ℕ) :
    max 1 (1/(sourceSamplingWidth stage*sourceSamplingCutoff stage)) ≤
      (sourceBlockSize stage : ℝ)^(3 : ℝ) := by
…
```
Mentions: OAI.FiniteFactor.sourceSamplingWidth, OAI.FiniteFactor.sourceSamplingCutoff, OAI.FiniteFactor.sourceBlockSize

theorem OAI.FiniteFactor.sourceSampling_second_pair_error line 32

Source documentation

Actual second-diagonal pair error for the selected source powers. All phase support, atomlessness and discrepancy hypotheses are discharged.

theorem sourceSampling_second_pair_error (stage : ℕ) (hs : 200000 ≤ sourceBlockSize stage)
    (i : SourceCoordinate) (hi : i.1 ≤ stage) (n n' : ℤ)
    (hn : n ∈ sourceSamplingPowers stage) (hn' : n' ∈ sourceSamplingPowers stage) (hne : n ≠ n')
    (G : Set ℝ) (hG : MeasurableSet G) (a c s : ℝ) (hsx : s ∈ Set.Ico (0 : ℝ) 1) :
    |(∫ θ, samplingTestedSecondWeight (sourceSamplingWidth stage) (sourceSamplingCutoff stage)
        (Set.Icc a c) G s (Int.fract ((n : ℝ)*θ i)) *
        samplingTestedSecondWeight (sourceSamplingWidth stage) (sourceSamplingCutoff stage)
        (Set.Icc a c) G s (Int.fract ((n' : ℝ)*θ i)) ∂sourceAngleLaw) -
      samplingTestedSecondDensity (sourceSamplingWidth stage) (sourceSamplingCutoff stage) (Set.Icc a c) G s ^ 2| ≤
      104*(sourceBlockSize stage : ℝ)^(-74 : ℝ) := by
…

Mentions: OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingPowers, OAI.FiniteFactor.samplingTestedSecondWeight, OAI.FiniteFactor.sourceSamplingWidth, OAI.FiniteFactor.sourceSamplingCutoff, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.samplingTestedSecondDensity