StartingMeasures.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Starting measures in all dimensions

The published input is Frostman's lemma, Mattila, Geometry of Sets and Measures in Euclidean Spaces (Cambridge, 1995), Theorem 8.8, p. 112. Only compact sets above the critical half-dimensional threshold are used. Selecting an exponent strictly between the threshold and the Hausdorff dimension, and normalizing the nonzero finite measure, gives the exact specialization below, stated as a hypothesis for the conditional argument.

The separation and restriction arguments are proved here in the original ambient dimension. They do not use a projection of the distance set.

def OAI.Falconer.FrostmanBallBound line 23
def OAI.Falconer.PublishedFrostmanAboveHalf line 28
Source documentation
Application-level specialization of Mattila (1995), Theorem 8.8. The upper bound on the exponent only fixes a convenient unit-size gap.
```
def PublishedFrostmanAboveHalf : Prop :=
…
```
theorem OAI.Falconer.noAtoms_of_frostman line 35
theorem OAI.Falconer.normalized_frostman_restriction line 49
theorem OAI.Falconer.distinct_support_points line 75
theorem OAI.Falconer.separated_compact_pieces line 90

theorem OAI.Falconer.starting_measures_of_published_frostman line 127

Source documentation

Compact separated starting laws with a fixed positive Frostman gap, constructed conditionally only on the cited classical Frostman lemma.

theorem starting_measures_of_published_frostman (hF : PublishedFrostmanAboveHalf)
    {d : ℕ} (hd : 2 ≤ d) (E : Set (Space d)) (hE : IsCompact E)
    (hDim : (d : ℝ≥0∞) / 2 < dimH E) :
    ∃ χ : ℝ, 0 < χ ∧ χ < 1 ∧ ∃ μ ν : ProbabilityMeasure (Space d),
      IsCompact (μ : Measure (Space d)).support ∧ IsCompact (ν : Measure (Space d)).support ∧
      (μ : Measure (Space d)).support ⊆ E ∧ (ν : Measure (Space d)).support ⊆ E ∧
      ∃ C r : ℝ, 0 < C ∧ 0 < r ∧ FrostmanBallBound (μ : Measure (Space d)) ((d : ℝ)/2 + χ) C ∧
        FrostmanBallBound (ν : Measure (Space d)) ((d : ℝ)/2 + χ) C ∧
        ∀ x ∈ (μ : Measure (Space d)).support, ∀ y ∈ (ν : Measure (Space d)).support,
          r/2 ≤ dist x y ∧ dist x y ≤ 2*r := by
…

Mentions: OAI.Falconer.PublishedFrostmanAboveHalf, OAI.Falconer.Space, OAI.Falconer.FrostmanBallBound