OAI/NumberTheory/DukePrimeDegree/Geometry/LeafMaximalIntrinsic.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Relative maximal estimates for intrinsic leaves in a root box

Normalization does not change a relative mass inequality. On an interval contained in a root box, the intrinsic leaf therefore gives the same relative bound as the box's conditional probability measure.

  1. lemma OAI.DukePrimeDegree.basedRealMeasure_translate_apply line 20
  2. lemma OAI.DukePrimeDegree.smul_relative_mass_iff line 36
  3. lemma OAI.DukePrimeDegree.basedRealMeasure_relative_mass_iff line 48
  4. lemma OAI.DukePrimeDegree.preimage_add_closedBall line 58
  5. lemma OAI.DukePrimeDegree.intrinsic_bad_interval_to_conditional line 65

    Source documentation

    If an intrinsic bad interval stays inside the root box, its relative mass inequality passes to the actual conditional kernel.

    lemma intrinsic_bad_interval_to_conditional
    {n : ℕ} {i j k : Fin n} (hij : i ≠ j)
    (A : RootBox hij k) (R : ℝ) (μ : Measure (X n)) [IsFiniteMeasure μ]
    (s : RootSlice i j k) (t r : ℝ) (E : Set (X n)) (hE : MeasurableSet E)
    (hs : A.IsNormalizedRootLeaf R μ s (A.leafMeasure R μ s))
    (ht : 0 < A.leafMeasure R μ s (ball t 1))
    (heq : intrinsicRootLeaf hij μ (rootQuotientParametrization hij (s, t)) =
      A.basedLeaf R μ (s, t))
    (hr : closedBall t r ⊆ A.time) (c : ℝ≥0∞)
    (hbad : c * intrinsicRootLeaf hij μ (rootQuotientParametrization hij (s, t))
        (closedBall 0 r) ≤
      intrinsicRootLeaf hij μ (rootQuotientParametrization hij (s, t))
…