OAI/NumberTheory/DukePrimeDegree/Entropy/CountableFutureMap.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DukePrimeDegree.entireFutureObservation line 20
2. lemma OAI.DukePrimeDegree.entireFutureObservation_measurable line 23
3. lemma OAI.DukePrimeDegree.countableFutureSigma_eq_comap line 28
4. lemma OAI.DukePrimeDegree.transverseCountableFutureSigma_eq_comap line 35
5. lemma OAI.DukePrimeDegree.countableFutureFiber_eq_of_mem line 50
6. theorem OAI.DukePrimeDegree.mem_future_event_iff line 63

   Source documentation

   Every event in the complete transverse-future sigma algebra is constant along its future fibers, with no exceptional set needed.

   theorem mem_future_event_iff {S V Y : Type*}
       [MeasurableSpace S] [MeasurableSpace V]
       (T : Y → Y) (Q : Y → ℕ) (F : S × V → Y)
       {E : Set (S × V)}
       (hE : MeasurableSet[⨆ m, transverseLabelSigma
         (fun z => countableFutureCode T Q m (F z))] E)
       (z : S × V) {u : V} (hu : u ∈ countableFutureFiber T Q F z) :
       (z.1,u) ∈ E ↔ z ∈ E := by
   …

   Mentions: OAI.DukePrimeDegree.transverseLabelSigma, OAI.DukePrimeDegree.countableFutureCode, OAI.DukePrimeDegree.countableFutureFiber

7. theorem OAI.DukePrimeDegree.measurable_countableFuture_mass line 82

   Source documentation

   Fiber masses of a kernel depending only on the transverse coordinate are measurable in the transverse-future sigma algebra itself. Thus mass conditions used to select boxes really are future events.

   theorem measurable_countableFuture_mass {S V Y : Type*}
       [MeasurableSpace S] [MeasurableSpace V] [MeasurableSpace Y]
       (κ : Kernel S V) [IsSFiniteKernel κ]
       {T : Y → Y} (hT : Measurable T) {Q : Y → ℕ} (hQ : Measurable Q)
       {F : S × V → Y} (hF : Measurable F)
       (A : Set (S × V)) (hA : MeasurableSet A) :
       Measurable[⨆ m, transverseLabelSigma (fun z => countableFutureCode T Q m (F z))]
         (fun z => κ z.1 ({t | (z.1,t) ∈ A} ∩ countableFutureFiber T Q F z)) := by
   …

   Mentions: OAI.DukePrimeDegree.transverseLabelSigma, OAI.DukePrimeDegree.countableFutureCode, OAI.DukePrimeDegree.countableFutureFiber

8. theorem OAI.DukePrimeDegree.measurableSet_future_mass_contained line 115

   Source documentation

   The event that a complete future fiber has no mass outside a fixed time domain is measurable using only the transverse coordinate and the future name.

   theorem measurableSet_future_mass_contained {S V Y : Type*}
       [MeasurableSpace S] [MeasurableSpace V] [MeasurableSpace Y]
       (κ : Kernel S V) [IsSFiniteKernel κ]
       {T : Y → Y} (hT : Measurable T) {Q : Y → ℕ} (hQ : Measurable Q)
       {F : S × V → Y} (hF : Measurable F)
       (B : Set V) (hB : MeasurableSet B) :
       MeasurableSet[⨆ m, transverseLabelSigma (fun z => countableFutureCode T Q m (F z))]
         {z | κ z.1 (countableFutureFiber T Q F z \ B) = 0} := by
   …

   Mentions: OAI.DukePrimeDegree.transverseLabelSigma, OAI.DukePrimeDegree.countableFutureCode, OAI.DukePrimeDegree.countableFutureFiber