OAI/Analysis/FiniteFactor/OrbitSampling/FirstMarginal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceSamplingUntrimmed_first_density line 13

   Source documentation

   The actual first marginal is the verified empirical interval-test density. The whole-circle tests [0,1] are valid on the Haar cube.

   theorem sourceSamplingUntrimmed_first_density (I : Finset SourceCoordinate) (stage : ℕ)
       (θ : SourceCoordinate → ℝ) :
       (sourceSamplingUntrimmed I stage θ).map Prod.fst =
         sourceSamplingHaar.withDensity (fun x => ENNReal.ofReal
           (sourceSamplingEmpiricalDensity stage false (fun i => decide (i ∈ I))
             (fun _ => Set.Icc 0 1) (fun _ => Set.Icc 0 1) θ x)) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingUntrimmed, OAI.FiniteFactor.sourceSamplingEmpiricalDensity

2. theorem OAI.FiniteFactor.sourceSamplingUntrimmed_first_L2 line 54

   Source documentation

   Uniform L2 densities for the actual untrimmed first marginals.

   theorem sourceSamplingUntrimmed_first_L2 (I : Finset SourceCoordinate) :
       ∀ᵐ θ ∂sourceAngleLaw, ∃ C : ℝ, ∀ stage,
         ∃ f : (SourceCoordinate → ℝ) → ℝ,
           (sourceSamplingUntrimmed I stage θ).map Prod.fst = sourceSamplingHaar.withDensity (fun x => ENNReal.ofReal (f x)) ∧
           MemLp f 2 sourceSamplingHaar ∧ (∫ x, f x^2 ∂sourceSamplingHaar) ≤ C := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.sourceSamplingUntrimmed, OAI.FiniteFactor.sourceSamplingHaar