OAI/NumberTheory/DukePrimeDegree/Geometry/LeafMaximalScaling.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Scaling relative bad intervals by the diagonal action

The actual canonical diagonal flow rescales root time by its exponential. Transport and projective normalization preserve every relative mass inequality used in the leafwise maximal argument.

  1. lemma OAI.DukePrimeDegree.normalized_map_image_relative_bound line 20
  2. lemma OAI.DukePrimeDegree.scaling_image_closedBall_zero line 34
  3. lemma OAI.DukePrimeDegree.rootCanonicalFlow_rescales_time line 45
  4. theorem OAI.DukePrimeDegree.intrinsic_bad_interval_scale line 70

    Source documentation

    A bad interval is sent to a bad interval of exponentially rescaled radius for the image set under the canonical diagonal flow.

    theorem intrinsic_bad_interval_scale
    (d : ℕ) {i j : Fin (d + 1)} (hij : i ≠ j)
    (μ : Measure (X (d + 1))) [IsFiniteMeasure μ]
    (x : X (d + 1)) (t r : ℝ) (E : Set (X (d + 1))) (hE : MeasurableSet E)
    (heq : intrinsicRootLeaf hij μ (rightAction x (rootCanonicalFlow d j t)) =
      anchorNormalize ((intrinsicRootLeaf hij μ x).map
        (Homeomorph.mulLeft₀ (Real.exp t) (Real.exp_ne_zero t))) (ball 0 1))
    (c : ℝ≥0∞)
    (hbad : c * intrinsicRootLeaf hij μ x (closedBall 0 r) ≤
      intrinsicRootLeaf hij μ x
        ({u | rightAction x (Matrix.SpecialLinearGroup.transvection hij u) ∈ E} ∩
          closedBall 0 r)) :
…