OAI/NumberTheory/DukePrimeDegree/Entropy/FiniteLabelEntropy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DukePrimeDegree.condExp_transverse_label_probability line 16
2. theorem OAI.DukePrimeDegree.conditionalEntropy_transverse_label line 52
3. theorem OAI.DukePrimeDegree.conditionalEntropy_transverse_label_restriction line 71

   Source documentation

   The entropy is computed from the actual leaf kernel, restricted to the observed fiber, with its measured normalization.

   theorem conditionalEntropy_transverse_label_restriction {M N : ℕ}
       (ρ : Measure (S × T)) [IsFiniteMeasure ρ]
       {P : S × T → Fin M} (hP : Measurable P)
       {Q : S × T → Fin N} (hQ : Measurable Q) :
       conditionalSigmaEntropy ρ P
           (MeasurableSpace.comap (fun z => (z.1,Q z))
             (inferInstance : MeasurableSpace (S × Fin N))) =
         ∫ z, observationEntropy
           ((anchorNormalize (ρ.condKernel z.1) {t | Q (z.1,t)=Q z}).restrict
             {t | Q (z.1,t)=Q z}) (fun t => P (z.1,t)) ∂ρ := by
   …