awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
⊢ eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
have neg : eLpNorm f p (μ.restrict s) ≤ ENNReal.ofReal ε
Tactic: rw [eLpNorm_indicator_eq_eLpNorm_restrict hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
⊢ ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
have h : ∀ (a : α), ‖f a‖ ≤ M
Tactic: filter_upwards
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
⊢ eLpNorm f p (μ.restrict s) ≤ ENNReal.ofReal ε
have haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
Tactic: have haebdd : ∀ᵐ x ∂μ.restrict s, ‖f x‖ ≤ M := by
    filter_upwards
    exact fun x => (hf x).le
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
⊢ eLpNorm f p (μ.restrict s) ≤ ENNReal.ofReal ε
have neg : HPow.hPow (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ * ENNReal.ofReal M ≤ ENNReal.ofReal ε
Tactic: refine le_trans (eLpNorm_le_of_ae_bound haebdd) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
⊢ HPow.hPow (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ * ENNReal.ofReal M ≤
    ENNReal.ofReal ε
have neg : HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) p.toReal⁻¹ ≤ ENNReal.ofReal ε / ENNReal.ofReal M
Tactic: rw [Measure.restrict_apply MeasurableSet.univ, Set.univ_inter,
    ← ENNReal.le_div_iff_mul_le (Or.inl _) (Or.inl ENNReal.ofReal_ne_top)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
neg : HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) p.toReal⁻¹ ≤ ENNReal.ofReal ε / ENNReal.ofReal M
⊢ HPow.hPow (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ * ENNReal.ofReal M ≤
    ENNReal.ofReal ε
have rw : ENNReal.ofReal M ≠ 0
Tactic: rw [Measure.restrict_apply MeasurableSet.univ, Set.univ_inter,
    ← ENNReal.le_div_iff_mul_le (Or.inl _) (Or.inl ENNReal.ofReal_ne_top)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
⊢ HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) p.toReal⁻¹ ≤ ENNReal.ofReal ε / ENNReal.ofReal M
have neg : (μ : (a : Set α) → ℝ≥0∞) s ≤ (ENNReal.ofReal ε / ENNReal.ofReal M) ^ p.toReal
Tactic: rw [ENNReal.rpow_inv_le_iff (ENNReal.toReal_pos hp hp_top)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
⊢ (μ : (a : Set α) → ℝ≥0∞) s ≤ (ENNReal.ofReal ε / ENNReal.ofReal M) ^ p.toReal
have neg : ENNReal.ofReal ((ε / M) ^ p.toReal) ≤ (ENNReal.ofReal ε / ENNReal.ofReal M) ^ p.toReal
Tactic: refine le_trans hμ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
⊢ ENNReal.ofReal ((ε / M) ^ p.toReal) ≤ (ENNReal.ofReal ε / ENNReal.ofReal M) ^ p.toReal
have neg : ENNReal.ofReal (ε / M) ^ p.toReal ≤ (ENNReal.ofReal ε / ENNReal.ofReal M) ^ p.toReal
Tactic: rw [← ENNReal.ofReal_rpow_of_pos (div_pos hε hM)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
⊢ ENNReal.ofReal (ε / M) ^ p.toReal ≤ (ENNReal.ofReal ε / ENNReal.ofReal M) ^ p.toReal
have neg : ENNReal.ofReal (ε / M) ≤ ENNReal.ofReal ε / ENNReal.ofReal M
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
⊢ ENNReal.ofReal (ε / M) ≤ ENNReal.ofReal ε / ENNReal.ofReal M
have neg : ENNReal.ofReal ε / ENNReal.ofReal M ≤ ENNReal.ofReal ε / ENNReal.ofReal M
Tactic: rw [ENNReal.ofReal_div_of_pos hM]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal ε
have obtain : ∀ (M : ℝ) (hMpos : 0 < M) (hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal ε
Tactic: obtain ⟨M, hMpos, hM⟩ := hf.eLpNorm_indicator_norm_ge_pos_le hmeas hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
x : α
⊢ ‖Set.indicator {x : α | ‖f x‖ < M} f x‖ < M
have rw : (if Membership.mem (γ := Set α) {x : α | ‖f x‖ < M} x then ‖f x‖ else 0) < M
Tactic: rw [norm_indicator_eq_indicator_norm, Set.indicator_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
x : α
⊢ (if Membership.mem (γ := Set α) {x : α | ‖f x‖ < M} x then ‖f x‖ else 0) < M
have pos : ∀ (h : Membership.mem (γ := Set α) {x : α | ‖f x‖ < M} x), ‖f x‖ < M
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
x : α
pos : ∀ (h : Membership.mem (γ := Set α) {x : α | ‖f x‖ < M} x), ‖f x‖ < M
⊢ (if Membership.mem (γ := Set α) {x : α | ‖f x‖ < M} x then ‖f x‖ else 0) < M
have neg : ∀ (h : x ∉ {x : α | ‖f x‖ < M}), 0 < M
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal ε
have obtain : ∀ (δ : ℝ) (hδpos : 0 < δ)
  (hδ :
    ∀ (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm (s.indicator (Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal ε
Tactic: obtain ⟨δ, hδpos, hδ⟩ :=
    eLpNorm_indicator_le_of_bound (f := { x | ‖f x‖ < M }.indicator f) hp_top hε (by
      intro x
      rw [norm_indicator_eq_indicator_norm, Set.indicator_apply]
      · split_ifs with h
        exacts [h, hMpos])
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator (Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal ε
have refine : ∀ (s : Set α) (hs : MeasurableSet s) (hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ),
  eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal ε
Tactic: refine ⟨δ, hδpos, fun s hs hμs => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator (Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal ε
have rw : eLpNorm (s.indicator (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f + Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤
  2 * ENNReal.ofReal ε
Tactic: rw [(_ : f = { x : α | M ≤ ‖f x‖₊ }.indicator f + { x : α | ‖f x‖ < M }.indicator f)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator (Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
rw :
  eLpNorm (s.indicator (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f + Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤
    2 * ENNReal.ofReal ε
⊢ eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal ε
have rw₁ : f = Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f + Set.indicator {x : α | ‖f x‖ < M} f
Tactic: rw [(_ : f = { x : α | M ≤ ‖f x‖₊ }.indicator f + { x : α | ‖f x‖ < M }.indicator f)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator (Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f + Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤
    2 * ENNReal.ofReal ε
have rw : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f + Set.indicator {x : α | ‖f x‖ < M} f) p (μ.restrict s) ≤
  2 * ENNReal.ofReal ε
Tactic: rw [eLpNorm_indicator_eq_eLpNorm_restrict hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator (Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
⊢ eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f + Set.indicator {x : α | ‖f x‖ < M} f) p (μ.restrict s) ≤
    2 * ENNReal.ofReal ε
have refine_1 : AEStronglyMeasurable (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) (μ.restrict s)
Tactic: refine le_trans (eLpNorm_add_le ?_ ?_ hp_one) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator (Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
refine_1 : AEStronglyMeasurable (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) (μ.restrict s)
⊢ eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f + Set.indicator {x : α | ‖f x‖ < M} f) p (μ.restrict s) ≤
    2 * ENNReal.ofReal ε
have refine_2 : AEStronglyMeasurable (Set.indicator {x : α | ‖f x‖ < M} f) (μ.restrict s)
Tactic: refine le_trans (eLpNorm_add_le ?_ ?_ hp_one) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator (Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
refine_1 : AEStronglyMeasurable (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) (μ.restrict s)
refine_2 : AEStronglyMeasurable (Set.indicator {x : α | ‖f x‖ < M} f) (μ.restrict s)
⊢ eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f + Set.indicator {x : α | ‖f x‖ < M} f) p (μ.restrict s) ≤
    2 * ENNReal.ofReal ε
have refine_3 : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p (μ.restrict s) +
    eLpNorm (Set.indicator {x : α | ‖f x‖ < M} f) p (μ.restrict s) ≤
  2 * ENNReal.ofReal ε
Tactic: refine le_trans (eLpNorm_add_le ?_ ?_ hp_one) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator (Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
⊢ eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p (μ.restrict s) +
      eLpNorm (Set.indicator {x : α | ‖f x‖ < M} f) p (μ.restrict s) ≤
    2 * ENNReal.ofReal ε
have refine_3 : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p (μ.restrict s) +
    eLpNorm (Set.indicator {x : α | ‖f x‖ < M} f) p (μ.restrict s) ≤
  ENNReal.ofReal ε + ENNReal.ofReal ε
Tactic: rw [two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator (Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
⊢ eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p (μ.restrict s) +
      eLpNorm (Set.indicator {x : α | ‖f x‖ < M} f) p (μ.restrict s) ≤
    ENNReal.ofReal ε + ENNReal.ofReal ε
have refine_3 : eLpNorm (Set.indicator {x : α | ‖f x‖ < M} f) p (μ.restrict s) ≤ ENNReal.ofReal ε
Tactic: refine add_le_add (le_trans (eLpNorm_mono_measure _ Measure.restrict_le_self) hM) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator (Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
⊢ eLpNorm (Set.indicator {x : α | ‖f x‖ < M} f) p (μ.restrict s) ≤ ENNReal.ofReal ε
have refine_3 : eLpNorm (s.indicator (Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
Tactic: rw [← eLpNorm_indicator_eq_eLpNorm_restrict hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator (Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
⊢ f = Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f + Set.indicator {x : α | ‖f x‖ < M} f
have h : ∀ (x : α), f x = (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f + Set.indicator {x : α | ‖f x‖ < M} f) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator (Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
x : α
⊢ f x = (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f + Set.indicator {x : α | ‖f x‖ < M} f) x
have pos : ∀ (hx : M ≤ ‖f x‖), f x = (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f + Set.indicator {x : α | ‖f x‖ < M} f) x
Tactic: by_cases hx : M ≤ ‖f x‖
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator (Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
x : α
pos : ∀ (hx : M ≤ ‖f x‖), f x = (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f + Set.indicator {x : α | ‖f x‖ < M} f) x
⊢ f x = (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f + Set.indicator {x : α | ‖f x‖ < M} f) x
have neg : ∀ (hx : ¬M ≤ ‖f x‖), f x = (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f + Set.indicator {x : α | ‖f x‖ < M} f) x
Tactic: by_cases hx : M ≤ ‖f x‖