OAI/Analysis/FiniteFactor/OrbitSampling/CrossProducts.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceSamplingIdealDensity_bounds line 11

   Source documentation

   A global bound used only to justify finite-stage integrations.

   theorem sourceSamplingIdealDensity_bounds (stage : ℕ) (r : Bool) (b : SourceCoordinate → Bool)
       (E G : SourceCoordinate → Set ℝ) (hE : ∀ i, MeasurableSet (E i)) (hG : ∀ i, MeasurableSet (G i))
       (x : SourceCoordinate → ℝ) :
       0 ≤ sourceSamplingIdealDensity stage r b E G x ∧
         sourceSamplingIdealDensity stage r b E G x ≤
           (max 1 (1/(sourceSamplingWidth stage*sourceSamplingCutoff stage)))^(sourceSamplingPrefix stage).card := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingIdealDensity, OAI.FiniteFactor.sourceSamplingWidth, OAI.FiniteFactor.sourceSamplingCutoff, OAI.FiniteFactor.sourceSamplingPrefix

2. theorem OAI.FiniteFactor.sourceSamplingProduct_mixed_factorization line 31

   Source documentation

   Exact mixed factorization for q_n and the actual ideal density on the full countable Haar space.

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

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

3. theorem OAI.FiniteFactor.sourceSamplingProduct_pair_integrable line 73

   Source documentation

   Fubini is justified for every finite-stage pair of actual summands.

   theorem sourceSamplingProduct_pair_integrable (stage : ℕ) (r : Bool) (b : SourceCoordinate → Bool)
       (E G : SourceCoordinate → Set ℝ) (hE : ∀ i, MeasurableSet (E i)) (hG : ∀ i, MeasurableSet (G i)) (n k : ℤ) :
       Integrable (fun p : (SourceCoordinate → ℝ) × (SourceCoordinate → ℝ) =>
         sourceSamplingProduct stage r b E G n p.1 p.2*sourceSamplingProduct stage r b E G k p.1 p.2)
         (sourceAngleLaw.prod (Measure.infinitePi (fun _ : SourceCoordinate => unitIntervalMeasure))) :=
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingProduct, OAI.FiniteFactor.unitIntervalMeasure

4. theorem OAI.FiniteFactor.sourceSamplingProduct_mixed_integrable line 84