-- Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
/-- If a function is supported on a finite-measure set and belongs to `ℒ^p`, then it belongs to
`ℒ^q` for any `q ≤ p`. -/
lemma MemLp.mono_exponent_of_measure_support_ne_top {p q : ℝ≥0∞} {f : α → E} (hfq : MemLp f q μ)
    {s : Set α} (hf : ∀ x, x ∉ s → f x = 0) (hs : μ s ≠ ∞) (hpq : p ≤ q) : MemLp f p μ

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
f : α → E
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ⊤
hpq : p ≤ q
⊢ (toMeasurable μ s).indicator f = f

Tactic:
apply Set.indicator_eq_self.2

Result:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
f : α → E
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ⊤
hpq : p ≤ q
⊢ Function.support f ⊆ toMeasurable μ s

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
f : α → E
s : Set α
hfq : MemLp f q (μ.restrict (toMeasurable μ s))
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ⊤
hpq : p ≤ q
this : (toMeasurable μ s).indicator f = f
⊢ MemLp f p (μ.restrict (toMeasurable μ s))

Tactic:
have : Fact (μ (toMeasurable μ s) < ∞) := ⟨by simpa [lt_top_iff_ne_top] using hs⟩

Result:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
f : α → E
s : Set α
hfq : MemLp f q (μ.restrict (toMeasurable μ s))
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ⊤
hpq : p ≤ q
this✝ : (toMeasurable μ s).indicator f = f
this : Fact (μ (toMeasurable μ s) < ⊤)
⊢ MemLp f p (μ.restrict (toMeasurable μ s))

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
f : α → E
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ⊤
hpq : p ≤ q
⊢ MemLp f p μ

Tactic:
have : (toMeasurable μ s).indicator f = f := by
  apply Set.indicator_eq_self.2
  apply Function.support_subset_iff'.2 fun x hx ↦ hf x ?_
  contrapose! hx
  exact subset_toMeasurable μ s hx

Result:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
f : α → E
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ⊤
hpq : p ≤ q
this : (toMeasurable μ s).indicator f = f
⊢ MemLp f p μ

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
f : α → E
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ⊤
hpq : p ≤ q
x : α
hx : x ∈ s
⊢ x ∈ toMeasurable μ s

Tactic:
exact subset_toMeasurable μ s hx

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
f : α → E
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ⊤
hpq : p ≤ q
this : (toMeasurable μ s).indicator f = f
⊢ MemLp f p μ

Tactic:
rw [← this, memLp_indicator_iff_restrict (measurableSet_toMeasurable μ s)] at hfq ⊢

Result:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
f : α → E
s : Set α
hfq : MemLp f q (μ.restrict (toMeasurable μ s))
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ⊤
hpq : p ≤ q
this : (toMeasurable μ s).indicator f = f
⊢ MemLp f p (μ.restrict (toMeasurable μ s))

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
f : α → E
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ⊤
hpq : p ≤ q
x : α
hx : x ∉ toMeasurable μ s
⊢ x ∉ s

Tactic:
contrapose! hx

Result:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
f : α → E
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ⊤
hpq : p ≤ q
x : α
hx : x ∈ s
⊢ x ∈ toMeasurable μ s

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
f : α → E
s : Set α
hfq : MemLp f q (μ.restrict (toMeasurable μ s))
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ⊤
hpq : p ≤ q
this✝ : (toMeasurable μ s).indicator f = f
this : Fact (μ (toMeasurable μ s) < ⊤)
⊢ MemLp f p (μ.restrict (toMeasurable μ s))

Tactic:
exact hfq.mono_exponent hpq

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
f : α → E
s : Set α
hfq : MemLp f q (μ.restrict (toMeasurable μ s))
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ⊤
hpq : p ≤ q
this : (toMeasurable μ s).indicator f = f
⊢ μ (toMeasurable μ s) < ⊤

Tactic:
simpa [lt_top_iff_ne_top] using hs

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
f : α → E
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ⊤
hpq : p ≤ q
⊢ Function.support f ⊆ toMeasurable μ s

Tactic:
apply Function.support_subset_iff'.2 fun x hx ↦ hf x ?_

Result:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p q : ℝ≥0∞
f : α → E
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ⊤
hpq : p ≤ q
x : α
hx : x ∉ toMeasurable μ s
⊢ x ∉ s