Infinite.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.FiniteFactor.CouplingParameters.CouplingSample line 13
Source documentation
The augmented countable product retains each coordinate's label and pair.
```
abbrev CouplingSample := ℕ → Fin 6 × (ℝ × ℝ)
```
def OAI.FiniteFactor.CouplingParameters.productCoupling line 15
instance OAI.FiniteFactor.CouplingParameters.productCoupling_probability line 18
def OAI.FiniteFactor.CouplingParameters.productEndpoint line 23
theorem OAI.FiniteFactor.CouplingParameters.productEndpoint_measurable line 26
theorem OAI.FiniteFactor.CouplingParameters.labelled_endpoint_density line 31
theorem OAI.FiniteFactor.CouplingParameters.productEndpoint_law line 41
Source documentation
Every coordinatewise choice of endpoint marginals is exactly its product law, including the mixed prefixes used in biased-identity.
```
theorem productEndpoint_law (p : ℕ → CouplingParameters) (right : ℕ → Bool) :
    (productCoupling p).map (productEndpoint right) =
      Measure.infinitePi (fun i => unitIntervalMeasure.withDensity
        (fun t => ENNReal.ofReal ((p i).endpointDensity (right i) t))) := by
…
```
Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.productCoupling, OAI.FiniteFactor.CouplingParameters.productEndpoint, OAI.FiniteFactor.CouplingParameters.endpointDensity
theorem OAI.FiniteFactor.CouplingParameters.productCoupling_cylinder line 51
Source documentation
Independence is recorded as the exact finite-cylinder product formula.
```
theorem productCoupling_cylinder (p : ℕ → CouplingParameters) (I : Finset ℕ)
    (S : ℕ → Set (Fin 6 × (ℝ × ℝ))) (hS : ∀ i ∈ I, MeasurableSet (S i)) :
    productCoupling p (Set.pi (I : Set ℕ) S) = ∏ i ∈ I, (p i).labelledCoupling (S i) :=
…
```
Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.productCoupling, OAI.FiniteFactor.CouplingParameters.labelledCoupling