OAI/Analysis/FiniteFactor/OrbitSampling/ProductMoments.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceSamplingProduct line 10
2. theorem OAI.FiniteFactor.sourceSamplingProduct_measurable line 16
3. theorem OAI.FiniteFactor.sourceSamplingProduct_bounds line 29
4. theorem OAI.FiniteFactor.sourceSamplingProduct_inner_factorization line 45

   Source documentation

   Exact coordinate factorization under the two actual infinite product laws. Dependence of the two phases within one coordinate is retained in each factor.

   theorem sourceSamplingProduct_inner_factorization (stage : ℕ) (r : Bool) (b : SourceCoordinate → Bool)
       (E G : SourceCoordinate → Set ℝ) (hE : ∀ i, MeasurableSet (E i)) (hG : ∀ i, MeasurableSet (G i)) (n k : ℤ) :
       (∫ x, ∫ θ, sourceSamplingProduct stage r b E G n θ x * sourceSamplingProduct stage r b E G k θ x
         ∂sourceAngleLaw ∂Measure.infinitePi (fun _ : SourceCoordinate => unitIntervalMeasure)) =
       ∏ i ∈ sourceSamplingPrefix stage,
         ∫ s, ∫ θ, samplingOrientedWeight r (b i) (sourceSamplingWidth stage) (sourceSamplingCutoff stage)
             (E i) (G i) s (Int.fract ((n : ℝ)*θ i)) *
           samplingOrientedWeight r (b i) (sourceSamplingWidth stage) (sourceSamplingCutoff stage)
             (E i) (G i) s (Int.fract ((k : ℝ)*θ i)) ∂sourceAngleLaw ∂unitIntervalMeasure := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingProduct, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.sourceSamplingPrefix, OAI.FiniteFactor.samplingOrientedWeight, OAI.FiniteFactor.sourceSamplingWidth, OAI.FiniteFactor.sourceSamplingCutoff

5. theorem OAI.FiniteFactor.sourceSamplingProduct_self_moment line 83

   Source documentation

   The actual full-prefix self-pair estimate, with the source's angle expectation outside the L2 square integral.

   theorem sourceSamplingProduct_self_moment (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 ^ 2
         ∂Measure.infinitePi (fun _ : SourceCoordinate => unitIntervalMeasure) ∂sourceAngleLaw) ≤
         (2+8*(sourceBlockSize stage : ℝ)^(3/5 : ℝ)*Real.log (sourceBlockSize stage : ℝ))^(sourceSamplingPrefix stage).card := by
   …

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