α : Type u_1
E : Type ?u.111298
F : Type ?u.111301
F' : Type ?u.111304
G : Type ?u.111307
𝕜 : Type ?u.111310
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = ⊤ → ↑↑μ' s = ⊤
⊢ DominatedFinMeasAdditive μ' T C
α : Type u_1
E : Type ?u.111298
F : Type ?u.111301
F' : Type ?u.111304
G : Type ?u.111307
𝕜 : Type ?u.111310
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
⊢ DominatedFinMeasAdditive μ' T C
have h' : ∀ s, MeasurableSet s → μ s = ∞ → μ' s = ∞ := by
  intro s hs hμs; rw [eq_top_iff, ← hμs]; exact h s hs
α : Type u_1
E : Type ?u.111298
F : Type ?u.111301
F' : Type ?u.111304
G : Type ?u.111307
𝕜 : Type ?u.111310
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = ⊤ → ↑↑μ' s = ⊤
s : Set α
hs : MeasurableSet s
hμ's : ↑↑μ' s < ⊤
⊢ ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ' s)
α : Type u_1
E : Type ?u.111298
F : Type ?u.111301
F' : Type ?u.111304
G : Type ?u.111307
𝕜 : Type ?u.111310
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = ⊤ → ↑↑μ' s = ⊤
⊢ DominatedFinMeasAdditive μ' T C
refine' ⟨hT.1.of_eq_top_imp_eq_top h', fun s hs hμ's => _⟩
α : Type u_1
E : Type ?u.111298
F : Type ?u.111301
F' : Type ?u.111304
G : Type ?u.111307
𝕜 : Type ?u.111310
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = ⊤ → ↑↑μ' s = ⊤
s : Set α
hs : MeasurableSet s
hμ's : ↑↑μ' s < ⊤
hμs : ↑↑μ s < ⊤
⊢ ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ' s)
α : Type u_1
E : Type ?u.111298
F : Type ?u.111301
F' : Type ?u.111304
G : Type ?u.111307
𝕜 : Type ?u.111310
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = ⊤ → ↑↑μ' s = ⊤
s : Set α
hs : MeasurableSet s
hμ's : ↑↑μ' s < ⊤
⊢ ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ' s)
have hμs : μ s < ∞ := (h s hs).trans_lt hμ's
α : Type u_1
E : Type ?u.111298
F : Type ?u.111301
F' : Type ?u.111304
G : Type ?u.111307
𝕜 : Type ?u.111310
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = ⊤ → ↑↑μ' s = ⊤
s : Set α
hs : MeasurableSet s
hμ's : ↑↑μ' s < ⊤
hμs : ↑↑μ s < ⊤
⊢ ENNReal.toReal (↑↑μ s) ≤ ENNReal.toReal (↑↑μ' s)
α : Type u_1
E : Type ?u.111298
F : Type ?u.111301
F' : Type ?u.111304
G : Type ?u.111307
𝕜 : Type ?u.111310
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = ⊤ → ↑↑μ' s = ⊤
s : Set α
hs : MeasurableSet s
hμ's : ↑↑μ' s < ⊤
hμs : ↑↑μ s < ⊤
⊢ ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ' s)
refine' (hT.2 s hs hμs).trans (mul_le_mul le_rfl _ ENNReal.toReal_nonneg hC)
α : Type u_1
E : Type ?u.111298
F : Type ?u.111301
F' : Type ?u.111304
G : Type ?u.111307
𝕜 : Type ?u.111310
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = ⊤ → ↑↑μ' s = ⊤
s : Set α
hs : MeasurableSet s
hμ's : ↑↑μ' s < ⊤
hμs : ↑↑μ s < ⊤
⊢ ↑↑μ s ≤ ↑↑μ' s
α : Type u_1
E : Type ?u.111298
F : Type ?u.111301
F' : Type ?u.111304
G : Type ?u.111307
𝕜 : Type ?u.111310
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = ⊤ → ↑↑μ' s = ⊤
s : Set α
hs : MeasurableSet s
hμ's : ↑↑μ' s < ⊤
hμs : ↑↑μ s < ⊤
⊢ ENNReal.toReal (↑↑μ s) ≤ ENNReal.toReal (↑↑μ' s)
rw [toReal_le_toReal hμs.ne hμ's.ne]
no goals
α : Type u_1
E : Type ?u.111298
F : Type ?u.111301
F' : Type ?u.111304
G : Type ?u.111307
𝕜 : Type ?u.111310
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = ⊤ → ↑↑μ' s = ⊤
s : Set α
hs : MeasurableSet s
hμ's : ↑↑μ' s < ⊤
hμs : ↑↑μ s < ⊤
⊢ ↑↑μ s ≤ ↑↑μ' s
exact h s hs
α : Type u_1
E : Type ?u.111298
F : Type ?u.111301
F' : Type ?u.111304
G : Type ?u.111307
𝕜 : Type ?u.111310
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s = ⊤
⊢ ↑↑μ' s = ⊤
α : Type u_1
E : Type ?u.111298
F : Type ?u.111301
F' : Type ?u.111304
G : Type ?u.111307
𝕜 : Type ?u.111310
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
⊢ ∀ (s : Set α), MeasurableSet s → ↑↑μ s = ⊤ → ↑↑μ' s = ⊤
intro s hs hμs
α : Type u_1
E : Type ?u.111298
F : Type ?u.111301
F' : Type ?u.111304
G : Type ?u.111307
𝕜 : Type ?u.111310
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s = ⊤
⊢ ↑↑μ s ≤ ↑↑μ' s
α : Type u_1
E : Type ?u.111298
F : Type ?u.111301
F' : Type ?u.111304
G : Type ?u.111307
𝕜 : Type ?u.111310
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s = ⊤
⊢ ↑↑μ' s = ⊤
rw [eq_top_iff, ← hμs]
no goals
α : Type u_1
E : Type ?u.111298
F : Type ?u.111301
F' : Type ?u.111304
G : Type ?u.111307
𝕜 : Type ?u.111310
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s = ⊤
⊢ ↑↑μ s ≤ ↑↑μ' s
exact h s hs