def increasingly_filtered {Z : Type u_5} [PartialOrder Z] (s : Set Z) : Prop

Equations

• increasingly_filtered s = ∀ U ∈ s, ∀ V ∈ s, ∃ W ∈ s, U ≤ W ∧ V ≤ W

def decreasingly_filtered {E : Type u_3} {ι : Type u_4} [e_frm : Order.Frame E] (V : ι → Sublocale E) : Prop

Equations

• decreasingly_filtered V = ∀ (n m : ι), ∃ (l : ι), V l ≤ V n ∧ V l ≤ V m

structure Measure {X : Type u_1} [h : Order.Frame X] : Type u_1

• toFun : Open X → NNReal
• empty : self.toFun ⊥ = 0
• mono (U V : Open X) : U ≤ V → self.toFun U ≤ self.toFun V
• strictly_additive (U V : Open X) : self.toFun (U ⊔ V) = self.toFun U + self.toFun V - self.toFun (U ⊓ V)
• filtered (s : Set (Open X)) : increasingly_filtered s → self.toFun (sSup s) = sSup (self.toFun '' s)

theorem Measure.strictly_additive'' {E : Type u_3} [e_frm : Order.Frame E] {m : Measure} (U V : Open E) : m.toFun U + m.toFun V = m.toFun (U ⊓ V) + m.toFun (U ⊔ V)

theorem Measure.strictly_additive' {E : Type u_3} [e_frm : Order.Frame E] {m : Measure} (U V : Open E) : m.toFun (U ⊓ V) = m.toFun U + m.toFun V - m.toFun (U ⊔ V)

theorem Measure.iSup_filtered {E : Type u_3} [e_frm : Order.Frame E] {m : Measure} {ι : Type u_5} (f : ι → Open E) : increasingly_filtered (Set.range f) → m.toFun (iSup f) = iSup (m.toFun ∘ f)

theorem Measure.monotone {E : Type u_3} [e_frm : Order.Frame E] {m : Measure} (u v : Open E) (h : u = v) : m.toFun u = m.toFun v

@[simp]

theorem Measure.all_le_top {X : Type u_1} [h : Order.Frame X] {m : Measure} (a : Open X) : m.toFun a ≤ m.toFun ⊤

noncomputable def Measure.caratheodory {X : Type u_1} [h : Order.Frame X] {m : Measure} (a : Sublocale X) : NNReal

Equations

• Measure.caratheodory a = sInf (m.toFun '' a.Open_Neighbourhood)

theorem Measure.caratheodory.open_eq_toFun {X : Type u_1} [h : Order.Frame X] {m : Measure} (x : Open X) : caratheodory x.toSublocale = m.toFun x

theorem Measure.caratheodory.top_eq_toFun {X : Type u_1} [h : Order.Frame X] {m : Measure} : caratheodory ⊤ = m.toFun ⊤

theorem Measure.caratheodory.mono {E : Type u_3} [e_frm : Order.Frame E] {m : Measure} {A B : Sublocale E} : A ≤ B → caratheodory A ≤ caratheodory B

theorem Measure.caratheodory.le_top {E : Type u_3} [e_frm : Order.Frame E] (m : Measure) (a : Sublocale E) : caratheodory a ≤ caratheodory ⊤

theorem Measure.caratheodory.le_top_toFun {E : Type u_3} [e_frm : Order.Frame E] (m : Measure) (a : Sublocale E) : caratheodory a ≤ m.toFun ⊤

theorem Measure.caratheodory.bot_eq_0 {E : Type u_3} [e_frm : Order.Frame E] (m : Measure) : caratheodory ⊥ = 0

theorem Exists_Neighbourhood_epsilon {E : Type u_3} [e_frm : Order.Frame E] {m : Measure} (a : Sublocale E) (ε : NNReal) : ε > 0 → ∃ w ∈ a.Open_Neighbourhood, m.toFun w ≤ Measure.caratheodory a + ε

theorem Exists_Neighbourhood_epsilon_lt {E : Type u_3} [e_frm : Order.Frame E] {m : Measure} (a : Sublocale E) (ε : NNReal) : ε > 0 → ∃ w ∈ a.Open_Neighbourhood, m.toFun w < Measure.caratheodory a + ε

def ℕpos : Type

Equations

• ℕpos = { n : ℕ // 0 < n }

def Rpos : Type

Equations

• Rpos = { r : NNReal // 0 < r }

theorem Measure.caratheodory.preserves_sup' {X : Type u_1} [h : Order.Frame X] (m : Measure) (X_n : ℕ → Sublocale X) : Monotone X_n → caratheodory (iSup X_n) = iSup (caratheodory ∘ X_n)

Leroy Lemme 1 -> Magie

theorem Measure.caratheodory.subadditive {E : Type u_3} [e_frm : Order.Frame E] {m : Measure} (a b : Sublocale E) : caratheodory (a ⊔ b) ≤ caratheodory a + caratheodory b