How constructive is constructing measures?

Pauly and Fouche

In the proof of Example 15 they write: let d be the restriction of the usual metric on Cantor space.

Here we specify what we think they meant by the usual metric on Cantor space.

We also include the Lebesgue measure on Cantor space as a Hausdorff measure, which is also relevant to their paper as "Particular attention is paid to Frostman measures on sets with positive Hausdorff dimension".

In theorem measure_univ_prototype we give a prototype of the argument from compactness that the Hausdorff measure of the whole space is 1.

noncomputable instance myInstance : MetricSpace (ℕ → Bool)

Equations

• myInstance = PiNat.metricSpaceOfDiscreteUniformity myInstance.proof_1

noncomputable def μ : MeasureTheory.Measure (ℕ → Bool)

Equations

• μ = MeasureTheory.Measure.hausdorffMeasure 1

theorem dist_one {t : ℕ → Bool} {f : ℕ → Bool} (h : t 0 ≠ f 0) : 1 = dist t f

If two members of Cantor space differ at 0 then their distance is 1.

theorem dist_of_diff {k : ℕ} {t : ℕ → Bool} {f : ℕ → Bool} (h : t k ≠ f k) : (1 / 2) ^ k ≤ dist t f

If two members of Cantor space differ at k then their distance is at least 2⁻ᵏ.

def fa : ℕ → Bool

Equations

• fa x = false

def tr : ℕ → Bool

Equations

• tr x = true

theorem dist_tf : 1 = dist tr fa

theorem dist_bound (x : ℕ → Bool) (y : ℕ → Bool) : dist x y ≤ 1

noncomputable def d : (ℕ → Bool) → (ℕ → Bool) → ℝ

Equations

• d = dist

noncomputable def de (x : ℕ → Bool) (y : ℕ → Bool) : ENNReal

Equations

• de x y = edist x y

noncomputable def F (t : ℕ → Bool) : ℝ

Equations

• F t = sSup (Set.range fun (y : ℕ → Bool) => d t y)

noncomputable def Fe (t : ℕ → Bool) : ENNReal

Equations

• Fe t = sSup (Set.range fun (y : ℕ → Bool) => de t y)

noncomputable def F_on (S : Set (ℕ → Bool)) (t : ℕ → Bool) : ℝ

Equations

• F_on S t = ⨆ y ∈ S, d t y

theorem de_d {x : ℕ → Bool} {y : ℕ → Bool} : (de x y).toReal = d x y

theorem ENNReal_div_pow {k : ℕ} : ((1 / 2) ^ k).toNNReal = (1 / 2) ^ k

theorem edist_of_diff {k : ℕ} {t : ℕ → Bool} {f : ℕ → Bool} (h : t k ≠ f k) : (1 / 2) ^ k ≤ edist t f

theorem sup_dist_bound (x : ℕ → Bool) : F x ≤ 1

theorem edist_bound (x : ℕ → Bool) (z : ℕ → Bool) : edist x z ≤ 1

theorem sup_edist_bound' (z : ℕ → Bool) : ⨆ (i : ℕ → Bool), edist i z ≤ 1

theorem sup_edist_lower_bound'1 {k : ℕ} (S : Set (ℕ → Bool)) (t : ℕ → Bool) (f : ℕ → Bool) (h₀ : t k ≠ f k) (h₁ : t ∈ S ∧ f ∈ S) : (1 / 2) ^ k ≤ ⨆ x ∈ S, ⨆ y ∈ S, edist x y

theorem sup_edist_lower_bound' (S : Set (ℕ → Bool)) (t : ℕ → Bool) (f : ℕ → Bool) (h₀ : t 0 ≠ f 0) (h₁ : t ∈ S ∧ f ∈ S) : 1 ≤ ⨆ x ∈ S, ⨆ y ∈ S, de x y

theorem sup_dist_lower_bound : 1 ≤ ⨆ x ∈ Set.univ, ⨆ y ∈ Set.univ, d x y

theorem sup_sup_dist_eq : ⨆ x ∈ Set.univ, ⨆ y ∈ Set.univ, dist x y = 1

theorem sub_edist_ne_top (i : ℕ → Bool) : (⨆ (y : ℕ → Bool), edist y) i ≠ ⊤

noncomputable def toReal_sup (x : ℕ → Bool) : ℝ

Equations

• toReal_sup x = (⨆ y ∈ Set.univ, edist x y).toReal

noncomputable def sup_toReal (x : ℕ → Bool) : ℝ

Equations

• sup_toReal x = ⨆ y ∈ Set.univ, (edist x y).toReal

theorem toReal_sup_eq_sup_toReal₀ (x : ℕ → Bool) : (⨆ y ∈ Set.univ, edist x y).toReal = ⨆ y ∈ Set.univ, (edist x y).toReal

theorem fubini : ⨆ (x : ℕ → Bool), ⨆ (y : ℕ → Bool), edist x y = ⨆ (y : ℕ → Bool), ⨆ (x : ℕ → Bool), edist x y

theorem fubini_toReal : ⨆ (x : ℕ → Bool), (⨆ (y : ℕ → Bool), edist x y).toReal = ⨆ (y : ℕ → Bool), (⨆ (x : ℕ → Bool), edist x y).toReal

theorem toReal_sup_sup_eq_sup_toReal_sup : (iSup (⨆ (y : ℕ → Bool), edist y)).toReal = ⨆ (i : ℕ → Bool), ((⨆ (y : ℕ → Bool), edist y) i).toReal

theorem toReal_sup_sup_eq_sup_toReal_sup' : (⨆ x ∈ Set.univ, ⨆ y ∈ Set.univ, edist x y).toReal = ⨆ x ∈ Set.univ, toReal_sup x

theorem diameter_one : Metric.diam Set.univ = 1

theorem e_diameter_one : EMetric.diam Set.univ = 1

theorem e_diameter_bound (S : Set (ℕ → Bool)) : EMetric.diam S ≤ 1

theorem diam_one (S : Set (ℕ → Bool)) (hS : ∃ (x : ℕ → Bool) (y : ℕ → Bool), x ∈ S ∧ y ∈ S ∧ x 0 = true ∧ y 0 = false) : EMetric.diam S = 1

theorem half_nonneg {k : ℕ} : 0 ≤ (1 / 2) ^ k

theorem ENNReal_simp {k : ℕ} : ↑((1 / 2) ^ k) = (1 / 2) ^ k

theorem NNReal_proof {k : ℕ} {half_nonneg_k : 0 ≤ (1 / 2) ^ k} : ↑⟨(1 / 2) ^ k, half_nonneg_k⟩ = ↑((1 / 2) ^ k)

theorem ENNReal_mess (k : ℕ) : ↑⟨(1 / 2) ^ k, ⋯⟩ = (1 / 2) ^ k

def ft : ℕ → Bool

Equations

• ft n = if n = 0 then false else if n = 1 then true else false

def ff : ℕ → Bool

Equations

• ff n = if n = 0 then false else if n = 1 then false else false

def tt (n : ℕ) : Bool

Equations

• tt n = if n = 0 then true else if n = 1 then true else false

def tf (n : ℕ) : Bool

Equations

• tf n = if n = 0 then true else if n = 1 then false else false

theorem edist_half {b : Bool} : ⨆ x ∈ {x : ℕ → Bool | x 0 = b}, ⨆ y ∈ {x : ℕ → Bool | x 0 = b}, edist x y ≤ 1 / 2

theorem one_or_other {S : Set (ℕ → Bool)} {T : Set (ℕ → Bool)} (hS : ¬∃ (x : ℕ → Bool) (y : ℕ → Bool), x ∈ S ∧ y ∈ S ∧ x 0 = true ∧ y 0 = false) (hT : ¬∃ (x : ℕ → Bool) (y : ℕ → Bool), x ∈ T ∧ y ∈ T ∧ x 0 = true ∧ y 0 = false) (h₀ : tr ∈ S ∨ tr ∈ T) (h₁ : fa ∈ S ∨ fa ∈ T) : tr ∈ S ↔ tr ∉ T

theorem four_sets_and_disjointness {S : Set (ℕ → Bool)} {T : Set (ℕ → Bool)} (h : Set.univ ⊆ S ∪ T) (hT : ¬∃ (x : ℕ → Bool) (y : ℕ → Bool), x ∈ T ∧ y ∈ T ∧ x 0 = true ∧ y 0 = false) (hl₀ : S ⊆ {x : ℕ → Bool | x 0 = false}) : S = {x : ℕ → Bool | x 0 = false} ∧ T = {x : ℕ → Bool | x 0 = true}

theorem measure_univ_prototype (S : Set (ℕ → Bool)) (T : Set (ℕ → Bool)) (h : Set.univ ⊆ S ∪ T) : 1 ≤ EMetric.diam S + EMetric.diam T