OAI/Analysis/FiniteFactor/Sampling/SecondMoment.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.samplingTransportDensity_bounds line 11
2. theorem OAI.FiniteFactor.samplingTransportDensity_integral line 34
3. def OAI.FiniteFactor.samplingVelocityMeasure line 54
4. theorem OAI.FiniteFactor.samplingVelocity_probability line 56
5. def OAI.FiniteFactor.samplingIdealSecond line 62

   Source documentation

   Actual averaged density of the uncut diagonal transport.

   def samplingIdealSecond (h s : ℝ) : ℝ :=
   …

6. theorem OAI.FiniteFactor.samplingIdealSecond_bounds line 65
7. theorem OAI.FiniteFactor.samplingIdealSecond_measurable line 96
8. theorem OAI.FiniteFactor.samplingIdealSecond_integral line 101

   Source documentation

   Fubini gives the exact mass identity for the averaged transport density.

   theorem samplingIdealSecond_integral (h : ℝ) (hh : 0 < h) (hh1 : h < 1) :
       (∫ s, samplingIdealSecond h s ∂unitIntervalMeasure) = 1 := by
   …

   Mentions: OAI.FiniteFactor.samplingIdealSecond, OAI.FiniteFactor.unitIntervalMeasure

9. theorem OAI.FiniteFactor.samplingIdealSecond_square line 124

   Source documentation

   The source's quadratic cancellation for the actual averaged uncut transport density. The exact mass-one identity eliminates the linear term.

   theorem samplingIdealSecond_square (h : ℝ) (hh : 0 < h) (hh1 : h < 1) :
       (∫ s, samplingIdealSecond h s^2 ∂unitIntervalMeasure) =
         1+(∫ s, (samplingIdealSecond h s-1)^2 ∂unitIntervalMeasure) ∧
       (∫ s, samplingIdealSecond h s^2 ∂unitIntervalMeasure) ≤ 1+h^2/(1-h)^2 := by
   …

   Mentions: OAI.FiniteFactor.samplingIdealSecond, OAI.FiniteFactor.unitIntervalMeasure