OAI/Analysis/FiniteFactor/OrbitSampling/TestedMarginals.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceSamplingEndpoint line 10
2. theorem OAI.FiniteFactor.sourceSamplingEndpoint_measurable line 14
3. theorem OAI.FiniteFactor.sourceSamplingSummand_tested_marginal line 20

   Source documentation

   Both actual rectangle-restricted marginal measures for a single power.

   theorem sourceSamplingSummand_tested_marginal (I : Finset SourceCoordinate) (stage : ℕ)
       (r : Bool) (E G : SourceCoordinate → Set ℝ)
       (hE : ∀ i, MeasurableSet (E i)) (hG : ∀ i, MeasurableSet (G i))
       (houtside : ∀ i ∉ sourceSamplingPrefix stage,
         Set.Ico (0 : ℝ) 1 ⊆ E i ∧ Set.Ico (0 : ℝ) 1 ⊆ G i)
       (θ : SourceCoordinate → ℝ) (n : ℤ) :
       ((sourceSamplingSummand I stage θ n).restrict (sourceSamplingRectangle E G)).map
           (sourceSamplingEndpoint r) =
         sourceSamplingHaar.withDensity (fun x => ENNReal.ofReal
           (sourceSamplingProduct stage r (fun i => decide (i ∈ I)) E G n θ x)) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingPrefix, OAI.FiniteFactor.sourceSamplingSummand, OAI.FiniteFactor.sourceSamplingRectangle, OAI.FiniteFactor.sourceSamplingEndpoint, OAI.FiniteFactor.sourceSamplingProduct

4. theorem OAI.FiniteFactor.sourceSamplingUntrimmed_tested_marginal line 50

   Source documentation

   Averaging commutes with rectangle restriction and either endpoint map. The density is the previously estimated empirical function, exactly.

   theorem sourceSamplingUntrimmed_tested_marginal (I : Finset SourceCoordinate) (stage : ℕ)
       (r : Bool) (E G : SourceCoordinate → Set ℝ)
       (hE : ∀ i, MeasurableSet (E i)) (hG : ∀ i, MeasurableSet (G i))
       (houtside : ∀ i ∉ sourceSamplingPrefix stage,
         Set.Ico (0 : ℝ) 1 ⊆ E i ∧ Set.Ico (0 : ℝ) 1 ⊆ G i)
       (θ : SourceCoordinate → ℝ) :
       ((sourceSamplingUntrimmed I stage θ).restrict (sourceSamplingRectangle E G)).map
           (sourceSamplingEndpoint r) =
         sourceSamplingHaar.withDensity (fun x => ENNReal.ofReal
           (sourceSamplingEmpiricalDensity stage r (fun i => decide (i ∈ I)) E G θ x)) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingPrefix, OAI.FiniteFactor.sourceSamplingUntrimmed, OAI.FiniteFactor.sourceSamplingRectangle, OAI.FiniteFactor.sourceSamplingEndpoint, OAI.FiniteFactor.sourceSamplingEmpiricalDensity