OAI/Analysis/FiniteFactor/Sampling/OrientedMoments.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.samplingOrientedWeight line 11

   Source documentation

   Both source orientations and both coordinate types, with exact x/y tests.

   def samplingOrientedWeight (second triangular : Bool) (h α : ℝ) (E G : Set ℝ) (s t : ℝ) : ℝ := by
   …

2. def OAI.FiniteFactor.samplingOrientedDensity line 17
3. theorem OAI.FiniteFactor.samplingOrientedWeight_measurable line 20
4. theorem OAI.FiniteFactor.samplingOrientedWeight_bounds line 32
5. theorem OAI.FiniteFactor.samplingOrientedWeight_triangular_bounds line 46
6. theorem OAI.FiniteFactor.samplingOrientedDensity_measurable line 52
7. theorem OAI.FiniteFactor.samplingOrientedDensity_triangular_bounds line 58

   Source documentation

   Both triangular orientations have tested marginal densities between zero and one.

   theorem samplingOrientedDensity_triangular_bounds (r : Bool) (h α : ℝ) (E G : Set ℝ)
       (hE : MeasurableSet E) (hG : MeasurableSet G) (s : ℝ) :
       0 ≤ samplingOrientedDensity r true h α E G s ∧
       samplingOrientedDensity r true h α E G s ≤ 1 := by
   …

   Mentions: OAI.FiniteFactor.samplingOrientedDensity

8. theorem OAI.FiniteFactor.samplingOrientedDensity_triangular_square line 72
9. theorem OAI.FiniteFactor.sourceSampling_oriented_moment line 82