OAI/Analysis/FiniteFactor/Sampling/SecondTriangular.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.samplingSecondTriangular_interval line 12

   Source documentation

   The triangular second orientation has one reflected interval of phases.

   theorem samplingSecondTriangular_interval (h α : ℝ) (G : Set ℝ) (a c s t : ℝ)
       (hs : s ∈ Set.Ico (0 : ℝ) 1) (ht : t ∈ Set.Ico (0 : ℝ) 1) :
       samplingOrientedWeight true true h α (Set.Icc a c) G s t =
         (Set.Ioc 0 s ∩ Set.Icc (s-c) (s-a)).indicator (fun _ => if s ∈ G then (1 : ℝ) else 0) t := by
   …

   Mentions: OAI.FiniteFactor.samplingOrientedWeight

2. theorem OAI.FiniteFactor.samplingSecondTriangular_reflect line 32

   Source documentation

   Reflection identifies the actual triangular second weight with a first weight. This equality concerns values; it introduces no new random law.

   theorem samplingSecondTriangular_reflect (h α : ℝ) (G : Set ℝ) (a c s t : ℝ)
       (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α)
       (hs : s ∈ Set.Ioo (0 : ℝ) 1) (ht : t ∈ Set.Ico (0 : ℝ) 1) (hts : t ≠ s) :
       samplingOrientedWeight true true h α (Set.Icc a c) G s t =
         samplingTestedFirstWeight true h α (if s ∈ G then Set.univ else ∅)
           (Set.Icc (1-c) (1-a)) (1-s) t := by
   …

   Mentions: OAI.FiniteFactor.samplingOrientedWeight, OAI.FiniteFactor.samplingTestedFirstWeight

3. theorem OAI.FiniteFactor.samplingSecondTriangular_pair_bound line 50

   Source documentation

   Rectangle discrepancy controls the remaining triangular second case.

   theorem samplingSecondTriangular_pair_bound {Ω : Type*} [MeasurableSpace Ω]
       (μ : Measure Ω) [IsProbabilityMeasure μ] (X Y : Ω → ℝ)
       (hX : Measurable X) (hY : Measurable Y)
       [NullSingletonClass (μ.map X)] [NullSingletonClass (μ.map Y)]
       (hXs : ∀ᵐ x ∂μ, X x ∈ Set.Ico (0 : ℝ) 1)
       (hYs : ∀ᵐ x ∂μ, Y x ∈ Set.Ico (0 : ℝ) 1)
       (δ : ℝ) (hδ : 0 ≤ δ) (hrect : ∀ a b c d : ℝ,
         |(μ {x | X x ∈ Set.Icc a b ∧ Y x ∈ Set.Icc c d}).toReal -
           (unitIntervalMeasure (Set.Icc a b)).toReal*(unitIntervalMeasure (Set.Icc c d)).toReal| ≤ δ)
       (h α : ℝ) (G : Set ℝ) (a c s : ℝ)
       (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α) (hs : s ∈ Set.Ioo (0 : ℝ) 1) :
       |(∫ x, samplingOrientedWeight true true h α (Set.Icc a c) G s (X x)*
   …

   Mentions: OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.samplingOrientedWeight