def e_μ {E : Type u_1} [Order.Frame E] (m : Measure) (u : E) : E

Equations

• e_μ m u = (sSup {w : Open E | u ≤ w.element ∧ m.toFun w = m.toFun { element := u }}).element

theorem e_μ_Measure_eq {E : Type u_1} [Order.Frame E] (m : Measure) (u : E) : m.toFun { element := e_μ m u } = m.toFun { element := u }

theorem e_μ_idempotent {E : Type u_1} [Order.Frame E] (m : Measure) (x : E) : e_μ m (e_μ m x) ≤ e_μ m x

theorem e_μ_le_apply {E : Type u_1} [Order.Frame E] (m : Measure) (x : E) : x ≤ e_μ m x

theorem e_μ_mono {E : Type u_1} [Order.Frame E] (m : Measure) (x y : E) : x ≤ y → e_μ m x ≤ e_μ m y

theorem e_μ_map_inf {E : Type u_1} [Order.Frame E] (m : Measure) (x y : E) : e_μ m (x ⊓ y) = e_μ m x ⊓ e_μ m y

def μ_Reduction {E : Type u_1} [Order.Frame E] (m : Measure) : Sublocale E

Equations

• μ_Reduction m = { toFun := e_μ m, map_inf' := ⋯, idempotent' := ⋯, le_apply' := ⋯ }

theorem Measure.μ_Reduction_le_if {E : Type u_1} [Order.Frame E] (m : Measure) (U : Sublocale E) : (∀ (i : E), m.toFun { element := U i } = m.toFun { element := i }) → μ_Reduction m ≤ U

theorem Measure_Neighbourhood_μ_eq_top {E : Type u_1} [Order.Frame E] (m : Measure) (V : Open E) : V ∈ (μ_Reduction m).Open_Neighbourhood → m.toFun V = m.toFun ⊤

theorem Measure_μ_Reduction_eq_top {E : Type u_1} [Order.Frame E] (m : Measure) : Measure.caratheodory (μ_Reduction m) = m.toFun ⊤

theorem μ_Reduction_eq_sInf {E : Type u_1} [Order.Frame E] [Fact (regular E)] (m : Measure) : μ_Reduction m = sInf (Open.toSublocale '' {w : Open E | m.toFun w = m.toFun ⊤})

theorem μ_Reduction_eq_sInf_Sublocale {E : Type u_1} [Order.Frame E] [Fact (regular E)] (m : Measure) : μ_Reduction m = sInf {w : Sublocale E | Measure.caratheodory w = m.toFun ⊤}

theorem μ_Reduction_le_of_top {E : Type u_1} [Order.Frame E] [Fact (regular E)] (m : Measure) (A : Sublocale E) (h : Measure.caratheodory A = m.toFun ⊤) : μ_Reduction m ≤ A

theorem embed_measure_open {E : Type u_1} [Order.Frame E] {m : Measure} [Fact (regular E)] (A : Sublocale E) (b : Open ↑(Image A)) : Measure.caratheodory (Sublocale.embed b.toSublocale) = (Measure.restrict_sublocale_measure A m).toFun b

theorem embed_measure {E : Type u_1} [Order.Frame E] {m : Measure} [Fact (regular E)] (A : Sublocale E) (b : Sublocale ↑(Image A)) : Measure.caratheodory (Sublocale.embed b) = Measure.caratheodory b

noncomputable def R_μ {E : Type u_1} [Order.Frame E] {m : Measure} [Fact (regular E)] (A : Sublocale E) : Sublocale E

Equations

• R_μ A = Sublocale.embed (μ_Reduction (Measure.restrict_sublocale_measure A m))

theorem μ_R_μ_eq {E : Type u_1} [Order.Frame E] {m : Measure} [Fact (regular E)] (A : Sublocale E) : Measure.caratheodory A = Measure.caratheodory (R_μ A)

theorem Measure.preserves_iInf {E : Type u_2} [Order.Frame E] [Fact (regular E)] {m : Measure} (V_n : ℕ → Open E) (h : Antitone V_n) : caratheodory (iInf (Open.toSublocale ∘ V_n)) = iInf (m.toFun ∘ V_n)

Leroy Lemma 6

theorem ENNReal.tendsto_atTop' {β : Type u_2} [Nonempty β] [SemilatticeSup β] {f : β → ENNReal} {a : ENNReal} (ha : a ≠ ⊤) : Filter.Tendsto f Filter.atTop (nhds a) ↔ ∀ ε > 0, ε ≠ ⊤ → ∃ (N : β), ∀ n ≥ N, f n ∈ Set.Icc (a - ε) (a + ε)

def rec' {E : Type u_2} [Order.Frame E] (seq : ℕ → Open E) : ℕ → Open E

Equations

• rec' seq 0 = seq 0
• rec' seq n.succ = seq (n + 1) ⊓ rec' seq n

theorem Measure.caratheodordy.preserves_iInf {E : Type u_2} [Order.Frame E] [Fact (regular E)] {m : Measure} {ι : Type u_3} [Nonempty ι] (A_i : ι → Sublocale E) (h : decreasingly_filtered A_i) : caratheodory (iInf A_i) = iInf (caratheodory ∘ A_i)

Leroy lemme 7

theorem Measure.caratheodory.strictly_additive {E : Type u_2} [Order.Frame E] [Fact (regular E)] {m : Measure} (A B : Sublocale E) : caratheodory (A ⊔ B) = caratheodory A + caratheodory B - caratheodory (A ⊓ B)

theorem Beispiel {E : Type u_2} [Order.Frame E] [Fact (regular E)] {m : Measure} (A B : Sublocale E) : Measure.caratheodory (A ⊔ B) = Measure.caratheodory A + Measure.caratheodory B - Measure.caratheodory (A ⊓ B)