OAI/Probability/InvariantIsing/Core/KernelRelativeEntropy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The conditional entropy identity needed for the finite Gaussian sampling path. Its nonnegative integral form also covers zero variances.

  1. def OAI.InvariantIsing.kernelRelativeEntropy line 20

    Source documentation

    A measurable version of conditional relative entropy, for dominated kernels.

    def kernelRelativeEntropy (κ η : Kernel X Y) [IsMarkovKernel κ] [IsMarkovKernel η]
    (x : X) : ℝ≥0∞ :=
…
  2. lemma OAI.InvariantIsing.measurable_kernelRelativeEntropy line 24
  3. lemma OAI.InvariantIsing.kernelRelativeEntropy_eq line 32
  4. lemma OAI.InvariantIsing.klDiv_compProd_same_left line 40
  5. lemma OAI.InvariantIsing.klDiv_compProd_integral line 56
  6. lemma OAI.InvariantIsing.klDiv_comp_le_integral line 63