RootPrefixCountableInformation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Countable present information in an actual root box

The conditional probability is first computed for the genuine box conditional kernel, then identified with the normalized intrinsic product at the sampled point. No genericity of the chart center is required.

lemma OAI.DukePrimeDegree.normalized_restriction_real_ratio line 21

Source documentation

The scalar used to normalize a box cancels from conditional probabilities.

lemma normalized_restriction_real_ratio {Y : Type*} [MeasurableSpace Y]
    (ν : Measure Y) (A B C : Set Y) (hB : MeasurableSet B) (hC : MeasurableSet C)
    (hA₀ : ν A ≠ 0) (hAtop : ν A ≠ ∞) :
    ((anchorNormalize ν A).restrict A).real B /
        ((anchorNormalize ν A).restrict A).real C =
      ν.real (B ∩ A) / ν.real (C ∩ A) := by
…

theorem OAI.DukePrimeDegree.RootPrefixBox.conditionalInformation_countableFuture_intrinsicProduct line 39

theorem OAI.DukePrimeDegree.RootPrefixBox.conditionalInformation_countableFuture_uncenteredIntrinsicProduct line 71

Source documentation

In unnormalized coordinates only the actual masses of the two nested future atoms remain; the arbitrary box normalization disappears.

theorem conditionalInformation_countableFuture_uncenteredIntrinsicProduct
    (B : RootPrefixBox C c hP₀ hf g) (R : ℝ) (hBR : B.time ⊆ c.remainingWindow R 0)
    (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d+1)) μ]
    {Q : X (d+1) → ℕ} (hQ : Measurable Q)
    {T : X (d+1) → X (d+1)} (hT : Measurable T)
    (hgood : ∀ᵐ x ∂μ, ∀ᶠ v in 𝓝 (completeRootChain (d+1)).zeroTime, ∀ k : ℕ,
      Q (T^[k] (rightAction x ((completeRootChain (d+1)).word v)))=Q (T^[k] x)) :
    let F := C.timeParam c hP₀ hf g
…

Mentions: OAI.DukePrimeDegree.RootPrefixBox, OAI.DukePrimeDegree.completeRootChain