ConditionalNameCovers.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Integrating finite-name covers over conditional probability kernels

Reference names may depend on the conditioning parameter. Errors need only lie in the bad sets almost surely for the corresponding conditional measure. Their integrated cost is measured by the actual kernel mixture.

theorem OAI.DukePrimeDegree.nameEntropy_le_reference_bad_sets line 20

theorem OAI.DukePrimeDegree.integral_nameEntropy_le_reference_bad_sets line 62

Source documentation

The conditional error estimate integrates against the actual law of the conditioning parameter. No joint measurability of the chosen reference labels is needed; only the conditional entropy and bad-set probabilities are integrated.

theorem integral_nameEntropy_le_reference_bad_sets
    {S Y α : Type*} [MeasurableSpace S] [MeasurableSpace Y]
    [MeasurableSpace α] [MeasurableSingletonClass α]
    [Fintype α] [Nonempty α] [DecidableEq α]
    (τ : Measure S) [IsProbabilityMeasure τ]
    (κ : Kernel S Y) [IsMarkovKernel κ] (N M : ℕ)
    (P : Y → Fin N → α) (hP : Measurable P)
    (r : S → Y → Fin M) (hr : ∀ s, Measurable (r s))
    (v : S → Fin M → Fin N → α) (B : Fin N → Set Y)
    (hB : ∀ i, MeasurableSet (B i))
    (hbad : ∀ᵐ s ∂τ, ∀ i, ∀ᵐ y ∂κ s, P y i ≠ v s (r s y) i → y ∈ B i)
    {δ : ℝ} (hδ : 0 < δ) (hδ1 : δ < 1) :
…

theorem OAI.DukePrimeDegree.conditionalSigmaEntropy_fst_le_reference_bad_sets line 103

Source documentation

In actual disintegration coordinates, the integrated bad-set cost is exactly the corresponding marginal mass of the original probability law.

theorem conditionalSigmaEntropy_fst_le_reference_bad_sets
    {S Y α : Type*} [MeasurableSpace S] [MeasurableSpace Y]
    [StandardBorelSpace Y] [Nonempty Y]
    [MeasurableSpace α] [MeasurableSingletonClass α]
    [Fintype α] [Nonempty α] [DecidableEq α]
    (ρ : Measure (S × Y)) [IsProbabilityMeasure ρ] (N M : ℕ)
    (P : Y → Fin N → α) (hP : Measurable P)
    (r : S → Y → Fin M) (hr : ∀ s, Measurable (r s))
    (v : S → Fin M → Fin N → α) (B : Fin N → Set Y)
    (hB : ∀ i, MeasurableSet (B i))
    (hbad : ∀ᵐ s ∂ρ.fst, ∀ i, ∀ᵐ y ∂ρ.condKernel s,
      P y i ≠ v s (r s y) i → y ∈ B i)
…