RootLeafLowerBound.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Typical root leaves have a linear lower mass bound

The property is expressed at countably many exponential radii. This makes it measurable and allows transfer through the actual root-box disintegration.

def OAI.DukePrimeDegree.HasDiscreteLinearLowerBound line 20
Source documentation
A finite constant bounds inverse small-ball mass along integer scales.
```
def HasDiscreteLinearLowerBound (ν : Measure ℝ) : Prop :=
…
```
lemma OAI.DukePrimeDegree.measurableSet_hasDiscreteLinearLowerBound line 25
lemma OAI.DukePrimeDegree.ae_basedRealMeasure_discrete_lower_bound line 40
lemma OAI.DukePrimeDegree.RootBox.ae_basedLeaf_discrete_lower_bound line 77
lemma OAI.DukePrimeDegree.RootBox.ae_intrinsicRootLeaf_discrete_lower_bound_restrict line 105

theorem OAI.DukePrimeDegree.ae_intrinsicRootLeaf_discrete_lower_bound line 120

Source documentation

The actual intrinsic root leaf has a linear lower mass bound at almost all base points. No entropy input is assumed.

theorem ae_intrinsicRootLeaf_discrete_lower_bound {n : ℕ} {i j : Fin n} (hij : i ≠ j)
    (μ : Measure (X n)) [IsFiniteMeasure μ]
    (hfree : ∀ᵐ x ∂μ, ∀ v : ℝ,
      rightAction x (Matrix.SpecialLinearGroup.transvection hij v) = x → v = 0) :
    ∀ᵐ x ∂μ, HasDiscreteLinearLowerBound (intrinsicRootLeaf hij μ x) := by
…

Mentions: OAI.DukePrimeDegree.HasDiscreteLinearLowerBound