[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
⊢ Set.Nonempty (↑Λ '' {f | ∀ (x : X), x ∈ K → 1 ≤ ↑f x})
[PROOFSTEP]
rw [nonempty_image_iff]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
⊢ Set.Nonempty {f | ∀ (x : X), x ∈ K → 1 ≤ ↑f x}
[PROOFSTEP]
use(1 : X →ᵇ ℝ≥0)
[GOAL]
case h
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
⊢ 1 ∈ {f | ∀ (x : X), x ∈ K → 1 ≤ ↑f x}
[PROOFSTEP]
intro x _
[GOAL]
case h
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
x : X
a✝ : x ∈ K
⊢ 1 ≤ ↑1 x
[PROOFSTEP]
simp only [BoundedContinuousFunction.coe_one, Pi.one_apply]
[GOAL]
case h
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
x : X
a✝ : x ∈ K
⊢ 1 ≤ 1
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
ε : ℝ≥0
εpos : 0 < ε
⊢ ∃ f, (∀ (x : X), x ∈ K → 1 ≤ ↑f x) ∧ ↑Λ f < rieszContentAux Λ K + ε
[PROOFSTEP]
obtain ⟨α, ⟨⟨f, f_hyp⟩, α_hyp⟩⟩ :=
  exists_lt_of_csInf_lt (rieszContentAux_image_nonempty Λ K) (lt_add_of_pos_right (rieszContentAux Λ K) εpos)
[GOAL]
case intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
ε : ℝ≥0
εpos : 0 < ε
α : ℝ≥0
α_hyp : α < rieszContentAux Λ K + ε
f : X →ᵇ ℝ≥0
f_hyp : f ∈ {f | ∀ (x : X), x ∈ K → 1 ≤ ↑f x} ∧ ↑Λ f = α
⊢ ∃ f, (∀ (x : X), x ∈ K → 1 ≤ ↑f x) ∧ ↑Λ f < rieszContentAux Λ K + ε
[PROOFSTEP]
refine' ⟨f, f_hyp.left, _⟩
[GOAL]
case intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
ε : ℝ≥0
εpos : 0 < ε
α : ℝ≥0
α_hyp : α < rieszContentAux Λ K + ε
f : X →ᵇ ℝ≥0
f_hyp : f ∈ {f | ∀ (x : X), x ∈ K → 1 ≤ ↑f x} ∧ ↑Λ f = α
⊢ ↑Λ f < rieszContentAux Λ K + ε
[PROOFSTEP]
rw [f_hyp.right]
[GOAL]
case intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
ε : ℝ≥0
εpos : 0 < ε
α : ℝ≥0
α_hyp : α < rieszContentAux Λ K + ε
f : X →ᵇ ℝ≥0
f_hyp : f ∈ {f | ∀ (x : X), x ∈ K → 1 ≤ ↑f x} ∧ ↑Λ f = α
⊢ α < rieszContentAux Λ K + ε
[PROOFSTEP]
exact α_hyp
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K1 K2 : Compacts X
⊢ rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2
[PROOFSTEP]
apply NNReal.le_of_forall_pos_le_add
[GOAL]
case h
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K1 K2 : Compacts X
⊢ ∀ (ε : ℝ≥0), 0 < ε → rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
[PROOFSTEP]
intro ε εpos
[GOAL]
case h
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
⊢ rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
[PROOFSTEP]
obtain ⟨f1, f_test_function_K1⟩ := exists_lt_rieszContentAux_add_pos Λ K1 (half_pos εpos)
[GOAL]
case h.intro
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →ᵇ ℝ≥0
f_test_function_K1 : (∀ (x : X), x ∈ K1 → 1 ≤ ↑f1 x) ∧ ↑Λ f1 < rieszContentAux Λ K1 + ε / 2
⊢ rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
[PROOFSTEP]
obtain ⟨f2, f_test_function_K2⟩ :=
  exists_lt_rieszContentAux_add_pos Λ K2
    (half_pos εpos)
      --let `f := f1 + f2` test function for the content of `K`
[GOAL]
case h.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →ᵇ ℝ≥0
f_test_function_K1 : (∀ (x : X), x ∈ K1 → 1 ≤ ↑f1 x) ∧ ↑Λ f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →ᵇ ℝ≥0
f_test_function_K2 : (∀ (x : X), x ∈ K2 → 1 ≤ ↑f2 x) ∧ ↑Λ f2 < rieszContentAux Λ K2 + ε / 2
⊢ rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
[PROOFSTEP]
have f_test_function_union : ∀ x ∈ K1 ⊔ K2, (1 : ℝ≥0) ≤ (f1 + f2) x :=
  by
  rintro x (x_in_K1 | x_in_K2)
  · exact le_add_right (f_test_function_K1.left x x_in_K1)
  ·
    exact
      le_add_left
        (f_test_function_K2.left x x_in_K2)
          --use that `Λf` is an upper bound for `λ(K1⊔K2)`
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →ᵇ ℝ≥0
f_test_function_K1 : (∀ (x : X), x ∈ K1 → 1 ≤ ↑f1 x) ∧ ↑Λ f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →ᵇ ℝ≥0
f_test_function_K2 : (∀ (x : X), x ∈ K2 → 1 ≤ ↑f2 x) ∧ ↑Λ f2 < rieszContentAux Λ K2 + ε / 2
⊢ ∀ (x : X), x ∈ K1 ⊔ K2 → 1 ≤ ↑(f1 + f2) x
[PROOFSTEP]
rintro x (x_in_K1 | x_in_K2)
[GOAL]
case inl
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →ᵇ ℝ≥0
f_test_function_K1 : (∀ (x : X), x ∈ K1 → 1 ≤ ↑f1 x) ∧ ↑Λ f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →ᵇ ℝ≥0
f_test_function_K2 : (∀ (x : X), x ∈ K2 → 1 ≤ ↑f2 x) ∧ ↑Λ f2 < rieszContentAux Λ K2 + ε / 2
x : X
x_in_K1 : x ∈ ↑K1
⊢ 1 ≤ ↑(f1 + f2) x
[PROOFSTEP]
exact le_add_right (f_test_function_K1.left x x_in_K1)
[GOAL]
case inr
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →ᵇ ℝ≥0
f_test_function_K1 : (∀ (x : X), x ∈ K1 → 1 ≤ ↑f1 x) ∧ ↑Λ f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →ᵇ ℝ≥0
f_test_function_K2 : (∀ (x : X), x ∈ K2 → 1 ≤ ↑f2 x) ∧ ↑Λ f2 < rieszContentAux Λ K2 + ε / 2
x : X
x_in_K2 : x ∈ ↑K2
⊢ 1 ≤ ↑(f1 + f2) x
[PROOFSTEP]
exact
  le_add_left
    (f_test_function_K2.left x x_in_K2)
      --use that `Λf` is an upper bound for `λ(K1⊔K2)`
[GOAL]
case h.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →ᵇ ℝ≥0
f_test_function_K1 : (∀ (x : X), x ∈ K1 → 1 ≤ ↑f1 x) ∧ ↑Λ f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →ᵇ ℝ≥0
f_test_function_K2 : (∀ (x : X), x ∈ K2 → 1 ≤ ↑f2 x) ∧ ↑Λ f2 < rieszContentAux Λ K2 + ε / 2
f_test_function_union : ∀ (x : X), x ∈ K1 ⊔ K2 → 1 ≤ ↑(f1 + f2) x
⊢ rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
[PROOFSTEP]
apply (rieszContentAux_le Λ f_test_function_union).trans (le_of_lt _)
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →ᵇ ℝ≥0
f_test_function_K1 : (∀ (x : X), x ∈ K1 → 1 ≤ ↑f1 x) ∧ ↑Λ f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →ᵇ ℝ≥0
f_test_function_K2 : (∀ (x : X), x ∈ K2 → 1 ≤ ↑f2 x) ∧ ↑Λ f2 < rieszContentAux Λ K2 + ε / 2
f_test_function_union : ∀ (x : X), x ∈ K1 ⊔ K2 → 1 ≤ ↑(f1 + f2) x
⊢ ↑Λ (f1 + f2) < rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
[PROOFSTEP]
rw [map_add]
  --use that `Λfi` are lower bounds for `λ(Ki) + ε/2`
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →ᵇ ℝ≥0
f_test_function_K1 : (∀ (x : X), x ∈ K1 → 1 ≤ ↑f1 x) ∧ ↑Λ f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →ᵇ ℝ≥0
f_test_function_K2 : (∀ (x : X), x ∈ K2 → 1 ≤ ↑f2 x) ∧ ↑Λ f2 < rieszContentAux Λ K2 + ε / 2
f_test_function_union : ∀ (x : X), x ∈ K1 ⊔ K2 → 1 ≤ ↑(f1 + f2) x
⊢ ↑Λ f1 + ↑Λ f2 < rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
[PROOFSTEP]
apply lt_of_lt_of_le (_root_.add_lt_add f_test_function_K1.right f_test_function_K2.right) (le_of_eq _)
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →ᵇ ℝ≥0
f_test_function_K1 : (∀ (x : X), x ∈ K1 → 1 ≤ ↑f1 x) ∧ ↑Λ f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →ᵇ ℝ≥0
f_test_function_K2 : (∀ (x : X), x ∈ K2 → 1 ≤ ↑f2 x) ∧ ↑Λ f2 < rieszContentAux Λ K2 + ε / 2
f_test_function_union : ∀ (x : X), x ∈ K1 ⊔ K2 → 1 ≤ ↑(f1 + f2) x
⊢ rieszContentAux Λ K1 + ε / 2 + (rieszContentAux Λ K2 + ε / 2) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
[PROOFSTEP]
rw [add_assoc, add_comm (ε / 2), add_assoc, add_halves ε, add_assoc]
