OAI/Analysis/FiniteFactor/Sampling/TestedSecondMoment.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.samplingTestedSecondWeight line 11

   Source documentation

   Exact x- and y-tests in the second diagonal orientation.

   def samplingTestedSecondWeight (h α : ℝ) (E G : Set ℝ) (s t : ℝ) : ℝ := by
   …

2. def OAI.FiniteFactor.samplingTestedSecondDensity line 15
3. theorem OAI.FiniteFactor.samplingTestedSecondWeight_measurable line 18
4. theorem OAI.FiniteFactor.samplingTestedSecondWeight_bounds line 26
5. theorem OAI.FiniteFactor.samplingTestedSecondDensity_measurable line 34
6. theorem OAI.FiniteFactor.samplingTestedSecondDensity_bounds line 39
7. theorem OAI.FiniteFactor.samplingTestedSecondDensity_square line 53