OAI/Analysis/FiniteFactor/OrbitSampling/TorusMarginals.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceTorusEndpoint line 12
2. theorem OAI.FiniteFactor.sourceTorusEndpoint_measurable line 14
3. theorem OAI.FiniteFactor.sourceSamplingTorus_marginal_transport line 19
4. theorem OAI.FiniteFactor.sourceSamplingTrimmed_torus_marginals_event line 33

   Source documentation

   The actual torus marginals, rather than only the representative-space marginals, have uniformly bounded L2 densities with respect to product Haar.

   theorem sourceSamplingTrimmed_torus_marginals_event : ∀ᵐ θ ∂sourceAngleLaw,
       ∀ (I : Finset SourceCoordinate) (r : Bool), ∃ C : ℝ, ∀ s,
         ∃ g : SourceTorus → ℝ,
           Measurable g ∧ (∀ z, 0 ≤ g z) ∧
           (sourceSamplingTrimmedTorus I s θ : Measure SourceSamplingTorus).map (sourceTorusEndpoint r) =
             sourceTorusHaar.withDensity (fun z => ENNReal.ofReal (g z)) ∧
           MemLp g 2 sourceTorusHaar ∧ (∫ z, g z^2 ∂sourceTorusHaar) ≤ C := by
   …

   Mentions: OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceTorus, OAI.FiniteFactor.sourceSamplingTrimmedTorus, OAI.FiniteFactor.SourceSamplingTorus, OAI.FiniteFactor.sourceTorusEndpoint, OAI.FiniteFactor.sourceTorusHaar