OAI/Analysis/FiniteFactor/Sampling/SelfMoment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.samplingWeight_square_slice line 11

   Source documentation

   Squaring the constant-height slice leaves its reciprocal interval length.

   theorem samplingWeight_square_slice (h α s : ℝ) (hh : 0 < h) (hh1 : h < 1)
       (hα : 0 < α) (hs : s ∈ Set.Ico (0 : ℝ) 1) :
       (∫ t, samplingWeight false h α s t ^ 2 ∂unitIntervalMeasure) =
         if α ≤ samplingDistance s then 1/(h*samplingDistance s) else 0 := by
   …

   Mentions: OAI.FiniteFactor.samplingWeight, OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.samplingDistance

2. theorem OAI.FiniteFactor.samplingDistance_cutoff_integral line 26

   Source documentation

   Exact logarithmic integral of the cutoff reciprocal distance.

   theorem samplingDistance_cutoff_integral (α : ℝ) (hα : 0 < α) (hα1 : α ≤ 1/2) :
       (∫ s, (if α ≤ samplingDistance s then (samplingDistance s)⁻¹ else 0)
         ∂unitIntervalMeasure) = 2*Real.log (1/(2*α)) := by
   …

   Mentions: OAI.FiniteFactor.samplingDistance, OAI.FiniteFactor.unitIntervalMeasure

3. theorem OAI.FiniteFactor.samplingWeight_square_integral line 78