OAI/Analysis/FiniteFactor/Sampling/SecondInterval.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.samplingSecondLength line 10
2. theorem OAI.FiniteFactor.samplingSecondWeight_support_iff line 12
3. theorem OAI.FiniteFactor.samplingSecondWeight_interval line 53

   Source documentation

   Exact reciprocal on the actual second-oriented support.

   theorem samplingSecondWeight_interval (h α s t : ℝ) (hh : 0 < h) (hh1 : h < 1)
       (hα : 0 < α) (hs : s ∈ Set.Ico (0 : ℝ) 1) (ht : t ∈ Set.Ico (0 : ℝ) 1) :
       samplingSecondWeight h α s t =
         if 0 < t ∧ t < samplingSecondLength h s ∧ α ≤ s-t ∧ s-t ≤ 1-α
         then 1/(h*samplingDistance (s-t)) else 0 := by
   …

   Mentions: OAI.FiniteFactor.samplingSecondWeight, OAI.FiniteFactor.samplingSecondLength, OAI.FiniteFactor.samplingDistance

4. theorem OAI.FiniteFactor.samplingTestedSecondWeight_interval line 73

   Source documentation

   The x-test intersects that support with a reflected interval, while the y-test is constant in the phase variable.

   theorem samplingTestedSecondWeight_interval (h α : ℝ) (G : Set ℝ) (a c s t : ℝ)
       (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α)
       (hs : s ∈ Set.Ico (0 : ℝ) 1) (ht : t ∈ Set.Ico (0 : ℝ) 1) :
       samplingTestedSecondWeight h α (Set.Icc a c) G s t =
         (Set.Ioo 0 (samplingSecondLength h s) ∩
           Set.Icc (max (s-(1-α)) (s-c)) (min (s-α) (s-a))).indicator
           (fun t => if s ∈ G then 1/(h*samplingDistance (s-t)) else 0) t := by
   …

   Mentions: OAI.FiniteFactor.samplingTestedSecondWeight, OAI.FiniteFactor.samplingSecondLength, OAI.FiniteFactor.samplingDistance