RootPrefixProductKernel.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Actual box kernels recovered from the intrinsic root product

The center of a box need not be a generic point. The formula below uses the product at the sampled point, translates it back, and normalizes on the actual time domain of the box.

def OAI.DukePrimeDegree.RootPrefixBox.uncenteredIntrinsicProduct line 30
Source documentation
The intrinsic product transported from the sampled point to the uncentered time coordinates of the box.
```
def uncenteredIntrinsicProduct (_A : RootPrefixBox C c hP hf g)
    (μ : Measure (X (d+1))) [IsFiniteMeasure μ]
    (z : (UpperRootTransverse (d+1) × T) × c.Time) : Measure c.Time :=
…
```
Mentions: OAI.DukePrimeDegree.RootPrefixBox, OAI.DukePrimeDegree.UpperRootTransverse
def OAI.DukePrimeDegree.RootPrefixBox.intrinsicProductConditional line 38
Source documentation
The normalized intrinsic-product description of a box conditional.
```
def intrinsicProductConditional (A : RootPrefixBox C c hP hf g)
    (μ : Measure (X (d+1))) [IsFiniteMeasure μ]
    (z : (UpperRootTransverse (d+1) × T) × c.Time) : Measure c.Time :=
…
```
Mentions: OAI.DukePrimeDegree.RootPrefixBox, OAI.DukePrimeDegree.UpperRootTransverse
theorem OAI.DukePrimeDegree.RootPrefixBox.ae_conditionalKernel_eq_intrinsicProduct line 43
theorem OAI.DukePrimeDegree.RootPrefixBox.ae_uncenteredIntrinsicProduct_mass line 56

theorem OAI.DukePrimeDegree.RootPrefixBox.conditionalEntropy_eq_intrinsicProduct line 73

Source documentation

Finite conditional entropy in an actual box is the information in its normalized intrinsic root product. The integral is over actual samples, so no genericity of the chosen chart center is required.

theorem conditionalEntropy_eq_intrinsicProduct
    (A : RootPrefixBox C c hP hf g) (R : ℝ) (hAR : A.time ⊆ c.remainingWindow R 0)
    (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d+1)) μ]
    {α : Type*} [Fintype α]
    (Q : (UpperRootTransverse (d+1) × T) × c.Time → α)
    (hQ : ∀ a, MeasurableSet {z | Q z = a}) :
    conditionalSigmaEntropy (A.coordinateMeasure μ) Q
        (MeasurableSpace.comap Prod.fst
          (inferInstance : MeasurableSpace (UpperRootTransverse (d+1) × T))) =
      ∫ z, observationEntropy (A.intrinsicProductConditional μ z)
        (fun t => Q (z.1,t)) ∂A.coordinateMeasure μ := by
…

Mentions: OAI.DukePrimeDegree.RootPrefixBox, OAI.DukePrimeDegree.UpperRootTransverse