OAI/Analysis/FiniteFactor/OrbitSampling/IdealProduct.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceSamplingPrefix_card line 10

   Source documentation

   The actual source prefix dimension, including the current block.

   theorem sourceSamplingPrefix_card (stage : ℕ) :
       (sourceSamplingPrefix stage).card = (sourceStageState stage).d+sourceBlockSize stage := by
   …

   Mentions: OAI.FiniteFactor.sourceSamplingPrefix, OAI.FiniteFactor.sourceStageState, OAI.FiniteFactor.sourceBlockSize

2. theorem OAI.FiniteFactor.sourceSamplingPrefix_card_bound line 18
3. theorem OAI.FiniteFactor.sourceSampling_prefix_quadratic_budget line 26

   Source documentation

   The small quadratic coordinate errors stay bounded in the growing prefix.

   theorem sourceSampling_prefix_quadratic_budget (stage : ℕ) :
       ((sourceSamplingPrefix stage).card : ℝ)*(4*(sourceBlockSize stage : ℝ)^(-6/5 : ℝ)) ≤ 5 := by
   …

   Mentions: OAI.FiniteFactor.sourceSamplingPrefix, OAI.FiniteFactor.sourceBlockSize

4. def OAI.FiniteFactor.sourceSamplingIdealDensity line 45
5. theorem OAI.FiniteFactor.sourceSamplingIdealDensity_measurable line 50
6. theorem OAI.FiniteFactor.sourceSamplingIdealDensity_square line 57

   Source documentation

   Exact product factorization of the ideal marginal's quadratic moment.

   theorem sourceSamplingIdealDensity_square (stage : ℕ) (r : Bool) (b : SourceCoordinate → Bool)
       (E G : SourceCoordinate → Set ℝ) (hE : ∀ i, MeasurableSet (E i)) (hG : ∀ i, MeasurableSet (G i)) :
       (∫ x, sourceSamplingIdealDensity stage r b E G x ^ 2
         ∂Measure.infinitePi (fun _ : SourceCoordinate => unitIntervalMeasure)) =
         ∏ i ∈ sourceSamplingPrefix stage,
           ∫ s, samplingOrientedDensity r (b i) (sourceSamplingWidth stage) (sourceSamplingCutoff stage) (E i) (G i) s ^ 2
             ∂unitIntervalMeasure := by
   …

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

7. theorem OAI.FiniteFactor.sourceSamplingIdealDensity_uniform_square line 70

   Source documentation

   Uniform-in-stage ideal marginal bound. The second orientation uses the quadratic cancellation established for the actual cutoff diagonal density.

   theorem sourceSamplingIdealDensity_uniform_square (stage : ℕ) (r : Bool) (b : SourceCoordinate → Bool)
       (E G : SourceCoordinate → Set ℝ) (hE : ∀ i, MeasurableSet (E i)) (hG : ∀ i, MeasurableSet (G i)) :
       (∫ x, sourceSamplingIdealDensity stage r b E G x ^ 2
         ∂Measure.infinitePi (fun _ : SourceCoordinate => unitIntervalMeasure)) ≤ Real.exp 5 := by
   …

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

8. theorem OAI.FiniteFactor.sourceSamplingIdealDensity_memLp line 87

   Source documentation

   Each ideal marginal is genuinely in L2; the preceding integral bound is therefore a norm bound, not an integral of a nonintegrable function.

   theorem sourceSamplingIdealDensity_memLp (stage : ℕ) (r : Bool) (b : SourceCoordinate → Bool)
       (E G : SourceCoordinate → Set ℝ) (hE : ∀ i, MeasurableSet (E i)) (hG : ∀ i, MeasurableSet (G i)) :
       MemLp (sourceSamplingIdealDensity stage r b E G) 2
         (Measure.infinitePi (fun _ : SourceCoordinate => unitIntervalMeasure)) := by
   …

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