AveragedTransport.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.samplingIdealSecond_lintegral line 11
Source documentation
ENNReal form of the constructed averaged density.
```
theorem samplingIdealSecond_lintegral (h s : ℝ) (hh : 0 < h) (hh1 : h < 1) :
    ENNReal.ofReal (samplingIdealSecond h s) =
      ∫⁻ v, ENNReal.ofReal (samplingTransportDensity v s) ∂samplingVelocityMeasure h := by
…
```
Mentions: OAI.FiniteFactor.samplingIdealSecond, OAI.FiniteFactor.samplingTransportDensity, OAI.FiniteFactor.samplingVelocityMeasure

theorem OAI.FiniteFactor.samplingTransport_average line 27

Source documentation

The average of the actual transport laws has density q_h.

theorem samplingTransport_average (h : ℝ) (hh : 0 < h) (hh1 : h < 1)
    (F : ℝ → ℝ≥0∞) (hF : Measurable F) :
    (∫⁻ z, ∫⁻ v, F (samplingTransport v z) ∂samplingVelocityMeasure h ∂unitIntervalMeasure) =
      ∫⁻ s, ENNReal.ofReal (samplingIdealSecond h s)*F s ∂unitIntervalMeasure := by
…

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

theorem OAI.FiniteFactor.samplingWeight_endpoint_domination line 60

Source documentation

An actual cutoff-weight endpoint estimate, with no assumed second-marginal identification. It holds against every measurable nonnegative test.

theorem samplingWeight_endpoint_domination (h α : ℝ)
    (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α)
    (F : ℝ → ℝ≥0∞) (hF : Measurable F) :
    (∫⁻ z, ∫⁻ t, ENNReal.ofReal (samplingWeight false h α z t)*F (z+t)
      ∂unitIntervalMeasure ∂unitIntervalMeasure) ≤
        ∫⁻ s, ENNReal.ofReal (samplingIdealSecond h s)*F s ∂unitIntervalMeasure := by
…

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