OAI/NumberTheory/DukePrimeDegree/Entropy/RootPredecessorInformation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DukePrimeDegree.kernel_label_information_eq_of_fiber_equiv line 15

   Source documentation

   Recoding on a stationary kernel fiber does not require measurable equality on its measure-valued label.

   theorem kernel_label_information_eq_of_fiber_equiv
       {Y S α β : Type*} [MeasurableSpace Y] [MeasurableSpace S]
       [MeasurableSpace α] [MeasurableSingletonClass α] [Countable α]
       [MeasurableSpace β] [MeasurableSingletonClass β] [Countable β]
       (μ : Measure Y) [IsFiniteMeasure μ] (κ : Kernel Y Y) [IsMarkovKernel κ]
       (F : Y → S) (hF : Measurable F) (hstat : μ.bind κ=μ)
       (hself : ∀ᵐ x ∂μ, ∀ᵐ y ∂κ x, κ y=κ x)
       (hconst : ∀ᵐ x ∂μ, ∀ᵐ y ∂κ x, F y=F x)
       (P : Y → α) (hP : Measurable P) (B : Y → β) (hB : Measurable B)
       (hequiv : ∀ x y, F x=F y → (P x=P y ↔ B x=B y)) :
       conditionalInformation μ P
           (MeasurableSpace.comap (fun x => (κ x,F x)) inferInstance) =ᵐ[μ]
   …

   Mentions: OAI.DukePrimeDegree.conditionalInformation

2. theorem OAI.DukePrimeDegree.EliminationChain.predecessor_root_information line 53

   Source documentation

   The same finite predecessor symbol used for the ambient entropy bound has exactly the root-information integral on the finer root fibers.

   theorem predecessor_root_information
       (d : ℕ) {P : Finset (Fin (d+1) × Fin (d+1))} {D : Finset (Fin (d+1))}
       (c : EliminationChain P D) (hP : InitialRootPattern P)
       (hf : c.finalEntries=allPositiveRoots (d+1))
       (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
       (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u))=μ)
       (ell : Fin (d+1) → ℝ) (hell : ∑ k, ell k=0)
       (Q : X (d+1) → ℕ) (hQ : Measurable Q)
       (κ : Kernel (X (d+1)) (X (d+1))) [IsMarkovKernel κ]
       (hstat : μ.bind κ=μ)
       (hself : ∀ᵐ x ∂μ, ∀ᵐ y ∂κ x, κ y=κ x)
       (hversion : ∀ᵐ x ∂μ, κ x=c.ambientFutureMeasure hP hf μ ell hell Q 1 x)
   …

   Mentions: OAI.DukePrimeDegree.EliminationChain, OAI.DukePrimeDegree.InitialRootPattern, OAI.DukePrimeDegree.allPositiveRoots, OAI.DukePrimeDegree.diagonalFlow