OAI/Analysis/FiniteFactor/Sampling/WeightTransport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.samplingWeight_displacement line 12

   Source documentation

   At each retained starting coordinate, the source weight is exactly the law of the displacement v times the distance to the endpoint.

   theorem samplingWeight_displacement (h α z : ℝ)
       (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α)
       (hz : z ∈ Set.Ico (0 : ℝ) 1) (hcut : α ≤ samplingDistance z) :
       unitIntervalMeasure.withDensity (fun t => ENNReal.ofReal (samplingWeight false h α z t)) =
         (samplingVelocityMeasure h).map (fun v => samplingDistance z * v) := by
   …

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

2. theorem OAI.FiniteFactor.samplingWeight_transport_integral line 45

   Source documentation

   Exact substitution t=v*Delta(z), at each retained starting point.

   theorem samplingWeight_transport_integral (h α z : ℝ)
       (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α)
       (hz : z ∈ Set.Ico (0 : ℝ) 1) (hcut : α ≤ samplingDistance z)
       (F : ℝ → ℝ≥0∞) (hF : Measurable F) :
       (∫⁻ t, ENNReal.ofReal (samplingWeight false h α z t)*F (z+t) ∂unitIntervalMeasure) =
         ∫⁻ v, F (samplingTransport v z) ∂samplingVelocityMeasure h := by
   …

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

3. theorem OAI.FiniteFactor.samplingWeight_transport_le line 64

   Source documentation

   Discarding the cutoff only increases the weighted endpoint law.

   theorem samplingWeight_transport_le (h α z : ℝ)
       (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α)
       (hz : z ∈ Set.Ico (0 : ℝ) 1) (F : ℝ → ℝ≥0∞) (hF : Measurable F) :
       (∫⁻ t, ENNReal.ofReal (samplingWeight false h α z t)*F (z+t) ∂unitIntervalMeasure) ≤
         ∫⁻ v, F (samplingTransport v z) ∂samplingVelocityMeasure h := by
   …

   Mentions: OAI.FiniteFactor.samplingWeight, OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.samplingTransport, OAI.FiniteFactor.samplingVelocityMeasure