DiagonalRootTubes.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Finite diagonal orbit tubes in a remaining root group

These are actual conjugation tubes, not assumed entropy partitions. Their information is computed exactly; the passage from these tubes to metric entropy is a separate step.

lemma OAI.DukePrimeDegree.exp_scaled_abs_lt_iff line 19
lemma OAI.DukePrimeDegree.finite_exp_scaled_abs_lt_iff line 25
def OAI.DukePrimeDegree.EliminationChain.remainingBackwardTube line 55
Source documentation
The tube followed by the backward diagonal orbit, with every remaining matrix entry bounded by exp (-ρ) through time N.
```
def remainingBackwardTube (_c : EliminationChain P D)
    (ell : Fin n → ℝ) (hell : ∑ i, ell i = 0) (ρ : ℝ) (N : ℕ) :
    Set (positiveRootGeneratedGroup (allPositiveRoots n \ P)) :=
…
```
Mentions: OAI.DukePrimeDegree.EliminationChain, OAI.DukePrimeDegree.positiveRootGeneratedGroup, OAI.DukePrimeDegree.allPositiveRoots
theorem OAI.DukePrimeDegree.EliminationChain.remainingBackwardTube_eq_rectangle line 62
theorem OAI.DukePrimeDegree.EliminationChain.remainingBackwardTube_measurableSet line 92
def OAI.DukePrimeDegree.EliminationChain.remainingBackwardTubeInformation line 102
Source documentation
Negative log mass of an actual finite-time diagonal tube in the intrinsic remaining-subgroup leaf.
```
def remainingBackwardTubeInformation (c : EliminationChain P D)
    (hP : InitialRootPattern P) (hf : c.finalEntries = allPositiveRoots n)
    (ell : Fin n → ℝ) (hell : ∑ i, ell i = 0) (ρ : ℝ) (N : ℕ)
    (μ : Measure (X n)) [IsFiniteMeasure μ] (x : X n) : ℝ :=
…
```
Mentions: OAI.DukePrimeDegree.EliminationChain, OAI.DukePrimeDegree.InitialRootPattern, OAI.DukePrimeDegree.allPositiveRoots
theorem OAI.DukePrimeDegree.EliminationChain.remainingBackwardTubeInformation_eq line 114
theorem OAI.DukePrimeDegree.EliminationChain.integrable_remainingBackwardTubeInformation line 132

theorem OAI.DukePrimeDegree.EliminationChain.integral_remainingBackwardTubeInformation line 144

Source documentation

The mean tube information is linear in time, with a constant depending only on its initial radius.

theorem integral_remainingBackwardTubeInformation (c : EliminationChain P D)
    (hP : InitialRootPattern P) (hf : c.finalEntries = allPositiveRoots (d+1))
    (ell : Fin (d+1) → ℝ) (hell : ∑ i, ell i = 0) (ρ : ℝ) (N : ℕ)
    (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u)) = μ) :
    (∫ x, c.remainingBackwardTubeInformation hP hf ell hell ρ N μ x ∂μ) =
      ρ * (∑ p : ↥(allPositiveRoots (d+1) \ P), canonicalRootCoefficient d μ p.val.1 p.val.2) +
      (N:ℝ) * (∑ p : ↥(allPositiveRoots (d+1) \ P),
        max (ell p.val.1-ell p.val.2) 0 * canonicalRootCoefficient d μ p.val.1 p.val.2) := by
…

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

theorem OAI.DukePrimeDegree.EliminationChain.tendsto_mean_remainingBackwardTubeInformation line 158

Source documentation

Every fixed initial radius gives the same mean information rate.

theorem tendsto_mean_remainingBackwardTubeInformation (c : EliminationChain P D)
    (hP : InitialRootPattern P) (hf : c.finalEntries = allPositiveRoots (d+1))
    (ell : Fin (d+1) → ℝ) (hell : ∑ i, ell i = 0) (ρ : ℝ)
    (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u)) = μ) :
    Tendsto (fun N : ℕ =>
      (∫ x, c.remainingBackwardTubeInformation hP hf ell hell ρ N μ x ∂μ) / (N:ℝ))
      atTop (𝓝 (∑ p : ↥(allPositiveRoots (d+1) \ P),
        max (ell p.val.1-ell p.val.2) 0 * canonicalRootCoefficient d μ p.val.1 p.val.2)) := by
…