Transport.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.unitInterval_split line 10
theorem OAI.FiniteFactor.map_interval_affine line 16
def OAI.FiniteFactor.samplingTransport line 32
Source documentation
The uncut diagonal model moves z by v times its endpoint distance.
```
def samplingTransport (v z : ℝ) : ℝ := z+v*samplingDistance z
```
Mentions: OAI.FiniteFactor.samplingDistance
def OAI.FiniteFactor.samplingTransportDensity line 35
Source documentation
Exact density of the two affine branches of the uncut transport.
```
def samplingTransportDensity (v s : ℝ) : ℝ :=
…
```
theorem OAI.FiniteFactor.samplingTransportDensity_measurable line 38

theorem OAI.FiniteFactor.samplingTransport_density line 45

Source documentation

This is the actual push-forward density, not an assumed ideal moment.

theorem samplingTransport_density (v : ℝ) (hv : 0 ≤ v) (hv1 : v < 1) :
    unitIntervalMeasure.map (samplingTransport v) =
      unitIntervalMeasure.withDensity (fun s => ENNReal.ofReal (samplingTransportDensity v s)) := by
…

Mentions: OAI.FiniteFactor.samplingTransport, OAI.FiniteFactor.samplingTransportDensity