FirstDiscrepancy.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.samplingTestedFirst_pair_bound line 12

Source documentation

Rectangle discrepancy passes exactly to the first-oriented tested weights.

theorem samplingTestedFirst_pair_bound {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) [IsProbabilityMeasure μ] (X Y : Ω → ℝ)
    (hX : Measurable X) (hY : Measurable Y)
    [NullSingletonClass (μ.map X)] [NullSingletonClass (μ.map Y)]
    (δ : ℝ) (hrect : ∀ a b c d : ℝ,
      |(μ {ω | X ω ∈ Set.Icc a b ∧ Y ω ∈ Set.Icc c d}).toReal -
        (unitIntervalMeasure (Set.Icc a b)).toReal*(unitIntervalMeasure (Set.Icc c d)).toReal| ≤ δ)
    (b : Bool) (h α : ℝ) (E : Set ℝ) (a c s : ℝ)
    (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α) (hs : s ∈ Set.Ico (0 : ℝ) 1) :
    |(∫ ω, samplingTestedFirstWeight b h α E (Set.Icc a c) s (X ω) *
        samplingTestedFirstWeight b h α E (Set.Icc a c) s (Y ω) ∂μ) -
      samplingTestedFirstDensity b h α E (Set.Icc a c) s ^ 2| ≤
…

Mentions: OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.samplingTestedFirstWeight, OAI.FiniteFactor.samplingTestedFirstDensity

theorem OAI.FiniteFactor.sourceSampling_phase_null_singletons line 67
Source documentation
The actual selected phase laws are atomless, despite possible dependence between two phases. Only their already proved marginal domination is used.
```
theorem sourceSampling_phase_null_singletons (stage : ℕ) (hs : 200000 ≤ sourceBlockSize stage)
    (i : SourceCoordinate) (hi : i.1 ≤ stage) (n : ℤ) (hn : n ∈ sourceSamplingPowers stage) :
    NullSingletonClass (sourceAngleLaw.map (fun θ => Int.fract ((n : ℝ)*θ i))) := by
…
```
Mentions: OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingPowers

theorem OAI.FiniteFactor.sourceSampling_first_pair_bound line 78

Source documentation

Actual first-tested pair discrepancy, with all probabilistic assumptions discharged by the source's deterministic separated powers.

theorem sourceSampling_first_pair_bound (stage : ℕ) (hs : 200000 ≤ sourceBlockSize stage)
    (i : SourceCoordinate) (hi : i.1 ≤ stage) (n n' : ℤ)
    (hn : n ∈ sourceSamplingPowers stage) (hn' : n' ∈ sourceSamplingPowers stage) (hne : n ≠ n')
    (b : Bool) (E : Set ℝ) (a c s : ℝ) (hsx : s ∈ Set.Ico (0 : ℝ) 1) :
    |(∫ θ, samplingTestedFirstWeight b (sourceSamplingWidth stage) (sourceSamplingCutoff stage)
        E (Set.Icc a c) s (Int.fract ((n : ℝ)*θ i)) *
        samplingTestedFirstWeight b (sourceSamplingWidth stage) (sourceSamplingCutoff stage)
        E (Set.Icc a c) s (Int.fract ((n' : ℝ)*θ i)) ∂sourceAngleLaw) -
      samplingTestedFirstDensity b (sourceSamplingWidth stage) (sourceSamplingCutoff stage) E (Set.Icc a c) s ^ 2| ≤
      (26*(sourceBlockSize stage : ℝ)^(-80 : ℝ))*
        (if s ∈ E then samplingFirstHeight b (sourceSamplingWidth stage) (sourceSamplingCutoff stage) s else 0)^2 := by
…

Mentions: OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingPowers, OAI.FiniteFactor.samplingTestedFirstWeight, OAI.FiniteFactor.sourceSamplingWidth, OAI.FiniteFactor.sourceSamplingCutoff, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.samplingTestedFirstDensity, OAI.FiniteFactor.samplingFirstHeight