RemainingProductKernel.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A measurable version of the actual remaining-root product

This supplies measurability of the mass of a whole future atom, rather than imposing measurability as an additional dynamical hypothesis.

theorem OAI.DukePrimeDegree.EliminationChain.exists_remainingTimeKernel line 21

Source documentation

The intrinsic product has an s-finite kernel version.

theorem exists_remainingTimeKernel (d : ℕ)
    {P : Finset (Fin (d+1) × Fin (d+1))} {D : Finset (Fin (d+1))}
    (c : EliminationChain P D) (hP : InitialRootPattern P)
    (hf : c.finalEntries = allPositiveRoots (d+1))
    (μ : Measure (X (d+1))) [IsFiniteMeasure μ]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u)) = μ) :
    ∃ κ : Kernel (X (d+1)) c.Time, IsSFiniteKernel κ ∧
      ∀ᵐ x ∂μ, κ x = c.remainingTimeProduct hP hf μ x := by
…

Mentions: OAI.DukePrimeDegree.EliminationChain, OAI.DukePrimeDegree.InitialRootPattern, OAI.DukePrimeDegree.allPositiveRoots, OAI.DukePrimeDegree.diagonalFlow

lemma OAI.DukePrimeDegree.EliminationChain.measurableSet_remainingFutureRelation line 46

theorem OAI.DukePrimeDegree.EliminationChain.aemeasurable_remainingFutureMass line 68

Source documentation

The mass of the entire future fiber is measurable up to the ambient null set on which intrinsic leaf measures may be chosen arbitrarily.

theorem aemeasurable_remainingFutureMass (d : ℕ)
    {P : Finset (Fin (d+1) × Fin (d+1))} {D : Finset (Fin (d+1))}
    (c : EliminationChain P D) (hP : InitialRootPattern P)
    (hf : c.finalEntries = allPositiveRoots (d+1))
    (μ : Measure (X (d+1))) [IsFiniteMeasure μ]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u)) = μ)
    (ell : Fin (d+1) → ℝ) (hell : ∑ k, ell k = 0) (Q : X (d+1) → ℕ)
    (hQ : Measurable Q) (m : ℕ) :
    AEMeasurable (fun x => c.remainingTimeProduct hP hf μ x
      (c.remainingFutureAtom ell hell Q m x)) μ := by
…

Mentions: OAI.DukePrimeDegree.EliminationChain, OAI.DukePrimeDegree.InitialRootPattern, OAI.DukePrimeDegree.allPositiveRoots, OAI.DukePrimeDegree.diagonalFlow