-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem norm_condExpIndL1_le (x : G) : ‖condExpIndL1 hm μ s x‖ ≤ (μ s).toReal * ‖x‖

Proof state:
case neg
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : ¬MeasurableSet s
⊢ ‖condExpIndL1 hm μ s x‖ ≤ (μ s).toReal * ‖x‖

Tactic:
simp_rw [condExpIndL1_of_not_measurableSet hs]

Result:
case neg
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : ¬MeasurableSet s
⊢ ‖0‖ ≤ (μ s).toReal * ‖x‖

Proof state:
case pos
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : MeasurableSet s
hμs : μ s = ⊤
⊢ 0 ≤ (μ s).toReal * ‖x‖

Tactic:
exact mul_nonneg ENNReal.toReal_nonneg (norm_nonneg _)

Result:
no goals

Proof state:
case neg
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : ¬MeasurableSet s
⊢ 0 ≤ (μ s).toReal * ‖x‖

Tactic:
exact mul_nonneg ENNReal.toReal_nonneg (norm_nonneg _)

Result:
no goals

Proof state:
case pos
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : MeasurableSet s
hμs : μ s = ⊤
⊢ ‖condExpIndL1 hm μ s x‖ ≤ (μ s).toReal * ‖x‖

Tactic:
rw [condExpIndL1_of_measure_eq_top hμs x, Lp.norm_zero]

Result:
case pos
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : MeasurableSet s
hμs : μ s = ⊤
⊢ 0 ≤ (μ s).toReal * ‖x‖

Proof state:
case pos
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : MeasurableSet s
⊢ ‖condExpIndL1 hm μ s x‖ ≤ (μ s).toReal * ‖x‖

Tactic:
by_cases hμs : μ s = ∞

Result:
case pos
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : MeasurableSet s
hμs : μ s = ⊤
⊢ ‖condExpIndL1 hm μ s x‖ ≤ (μ s).toReal * ‖x‖

case neg
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : MeasurableSet s
hμs : ¬μ s = ⊤
⊢ ‖condExpIndL1 hm μ s x‖ ≤ (μ s).toReal * ‖x‖

Proof state:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
⊢ ‖condExpIndL1 hm μ s x‖ ≤ (μ s).toReal * ‖x‖

Tactic:
by_cases hs : MeasurableSet s

Result:
case pos
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : MeasurableSet s
⊢ ‖condExpIndL1 hm μ s x‖ ≤ (μ s).toReal * ‖x‖

case neg
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : ¬MeasurableSet s
⊢ ‖condExpIndL1 hm μ s x‖ ≤ (μ s).toReal * ‖x‖

Proof state:
case pos
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : MeasurableSet s
⊢ ‖condExpIndL1 hm μ s x‖ ≤ (μ s).toReal * ‖x‖

case neg
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : ¬MeasurableSet s
⊢ ‖condExpIndL1 hm μ s x‖ ≤ (μ s).toReal * ‖x‖

Tactic:
swap

Result:
case neg
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : ¬MeasurableSet s
⊢ ‖condExpIndL1 hm μ s x‖ ≤ (μ s).toReal * ‖x‖

case pos
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : MeasurableSet s
⊢ ‖condExpIndL1 hm μ s x‖ ≤ (μ s).toReal * ‖x‖

Proof state:
case neg
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : MeasurableSet s
hμs : ¬μ s = ⊤
⊢ ‖condExpIndL1Fin hm hs hμs x‖ ≤ (μ s).toReal * ‖x‖

Tactic:
exact norm_condExpIndL1Fin_le hs hμs x

Result:
no goals

Proof state:
case neg
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : ¬MeasurableSet s
⊢ ‖0‖ ≤ (μ s).toReal * ‖x‖

Tactic:
rw [Lp.norm_zero]

Result:
case neg
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : ¬MeasurableSet s
⊢ 0 ≤ (μ s).toReal * ‖x‖

Proof state:
case neg
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : MeasurableSet s
hμs : ¬μ s = ⊤
⊢ ‖condExpIndL1 hm μ s x‖ ≤ (μ s).toReal * ‖x‖

Tactic:
rw [condExpIndL1_of_measurableSet_of_measure_ne_top hs hμs x]

Result:
case neg
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : MeasurableSet s
hμs : ¬μ s = ⊤
⊢ ‖condExpIndL1Fin hm hs hμs x‖ ≤ (μ s).toReal * ‖x‖