awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
r : ℝ
u : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
x : α
h :
  (↑(f x) : ℝ≥0∞) ≠ 0 →
    (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
      (r • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E)) x
h' :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
h'' :
  (↑(↑(r • MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    (r •
        (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                  ⋯) :
              α →ₘ[μ] E) :
          α → E))
      x
h''' :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
h₁ :
  ∀ (hx : f x = 0),
    f x • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
      r • f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
⊢ f x • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
    r • f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
have h₂ : ∀ (hx : f x ≠ 0),
  f x • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
    r • f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
Tactic: rcases eq_or_ne (f x) 0 with (hx | hx)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
r : ℝ
u : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
x : α
h :
  (↑(f x) : ℝ≥0∞) ≠ 0 →
    (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
      (r • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E)) x
h' :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
h'' :
  (↑(↑(r • MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    (r •
        (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                  ⋯) :
              α →ₘ[μ] E) :
          α → E))
      x
h''' :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
hx : f x ≠ 0
⊢ f x • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x =
    r • f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
have rw : (↑(f x) : ℝ≥0∞) ≠ 0
Tactic: rw [h _, smul_comm, Pi.smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
⊢ norm (E := ↥(Lp E 1 μ))
      (({
              toFun := fun (u : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))) ↦
                MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                  ⋯,
              map_add' := ⋯, map_smul' := ⋯ :
              ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))) →ₗ[ℝ] ↥(Lp E 1 μ) } :
            (a : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))) → ↥(Lp E 1 μ))
          u :
        ↥(Lp E 1 μ)) =
    ‖u‖
have simp : (∫⁻ (a : α),
      ‖(↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                    sorry) :
                α →ₘ[μ] E) :
            α → E)
          a‖ₑ ∂μ).toReal =
  (∫⁻ (a : α),
      ‖(↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E)
          a‖ₑ ∂μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)).toReal
Tactic: simp only [eLpNorm, LinearMap.coe_mk, AddHom.coe_mk,
      one_ne_zero, ENNReal.one_ne_top, ENNReal.toReal_one, if_false, eLpNorm', ENNReal.rpow_one,
      _root_.div_one, Lp.norm_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
⊢ (∫⁻ (a : α),
        ‖(↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                      ⋯) :
                  α →ₘ[μ] E) :
              α → E)
            a‖ₑ ∂μ).toReal =
    (∫⁻ (a : α),
        ‖(↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E)
            a‖ₑ ∂μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)).toReal
have rw : (∫⁻ (a : α),
      ‖(↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                    sorry) :
                α →ₘ[μ] E) :
            α → E)
          a‖ₑ ∂μ).toReal =
  (∫⁻ (a : α),
      HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
        (fun (a : α) ↦ ‖(↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) a‖ₑ) a ∂μ).toReal
Tactic: rw [lintegral_withDensity_eq_lintegral_mul_non_measurable _ f_meas.coe_nnreal_ennreal
        (Filter.Eventually.of_forall fun x => ENNReal.coe_lt_top)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
⊢ (∫⁻ (a : α),
        ‖(↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                      ⋯) :
                  α →ₘ[μ] E) :
              α → E)
            a‖ₑ ∂μ).toReal =
    (∫⁻ (a : α),
        HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
          (fun (a : α) ↦ ‖(↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) a‖ₑ) a ∂μ).toReal
have e_a : ∫⁻ (a : α),
    ‖(↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) sorry) :
              α →ₘ[μ] E) :
          α → E)
        a‖ₑ ∂μ =
  ∫⁻ (a : α),
    HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
      (fun (a : α) ↦ ‖(↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) a‖ₑ) a ∂μ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
⊢ ∫⁻ (a : α),
      ‖(↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                    ⋯) :
                α →ₘ[μ] E) :
            α → E)
          a‖ₑ ∂μ =
    ∫⁻ (a : α),
      HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
        (fun (a : α) ↦ ‖(↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) a‖ₑ) a ∂μ
have e_a : (fun (a : α) ↦
    ‖(↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) sorry) :
              α →ₘ[μ] E) :
          α → E)
        a‖ₑ) =ᶠ[ae μ]
  HMul.hMul (α := α → ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) fun (a : α) ↦
    ‖(↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) a‖ₑ
Tactic: apply lintegral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
⊢ (fun (a : α) ↦
      ‖(↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                    ⋯) :
                α →ₘ[μ] E) :
            α → E)
          a‖ₑ) =ᶠ[ae μ]
    HMul.hMul (α := α → ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) fun (a : α) ↦
      ‖(↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) a‖ₑ
have h : ∀ (x : α)
  (hx :
    (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) sorry) :
              α →ₘ[μ] E) :
          α → E)
        x =
      f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x),
  ‖(↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) sorry) :
              α →ₘ[μ] E) :
          α → E)
        x‖ₑ =
    HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
      (fun (a : α) ↦ ‖(↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) a‖ₑ) x
Tactic: filter_upwards [(memL1_smul_of_L1_withDensity f_meas u).coeFn_toLp] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
x : α
hx :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
⊢ ‖(↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
              α →ₘ[μ] E) :
          α → E)
        x‖ₑ =
    HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
      (fun (a : α) ↦ ‖(↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) a‖ₑ) x
have h : ‖f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x‖ₑ =
  HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
    (fun (a : α) ↦ ‖(↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) a‖ₑ) x
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ (f x).toReal) 1 μ
have rw : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (f x).toReal) μ ∧ ∫⁻ (x : α), ‖(f x).toReal‖ₑ ∂μ < ∞
Tactic: rw [MemLp, eLpNorm_one_eq_lintegral_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ ↔ ∫⁻ (x : α), f x ∂μ ≠ ∞
have rw : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (f x).toReal) μ ∧ ∫⁻ (x : α), f x ∂μ ≠ ∞ ↔ ∫⁻ (x : α), f x ∂μ ≠ ∞
Tactic: rw [Integrable, hasFiniteIntegral_toReal_iff hf_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfm : AEStronglyMeasurable f μ
hf : 0 ≤ᶠ[ae μ] f
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ ≠ ∞ ↔ Integrable f μ
have rw : ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ ≠ ∞ ↔ AEStronglyMeasurable f μ ∧ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ∞
Tactic: rw [Integrable, hasFiniteIntegral_iff_ofReal hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ max (f a) 0) μ
have left : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ max (f a) 0) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
left : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ max (f a) 0) μ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ max (f a) 0) μ
have right : HasFiniteIntegral (ε := ℝ) (fun (a : α) ↦ max (f a) 0) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedAddCommGroup 𝕜
inst_2 : SMulZeroClass 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : Integrable f μ
⊢ Integrable (c • f) μ
have left : AEStronglyMeasurable (c • f) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedAddCommGroup 𝕜
inst_2 : SMulZeroClass 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : Integrable f μ
left : AEStronglyMeasurable (c • f) μ
⊢ Integrable (c • f) μ
have right : HasFiniteIntegral (c • f) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
ε : Type u_9
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
inst_2 : NormedAddCommGroup 𝕜
inst_3 : SMul 𝕜 ε
inst_4 : ContinuousConstSMul 𝕜 ε
inst_5 : ENormSMulClass 𝕜 ε
c : 𝕜
f : α → ε
hf : Integrable f μ
⊢ Integrable (c • f) μ
have left : AEStronglyMeasurable (c • f) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
ε : Type u_9
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
inst_2 : NormedAddCommGroup 𝕜
inst_3 : SMul 𝕜 ε
inst_4 : ContinuousConstSMul 𝕜 ε
inst_5 : ENormSMulClass 𝕜 ε
c : 𝕜
f : α → ε
hf : Integrable f μ
left : AEStronglyMeasurable (c • f) μ
⊢ Integrable (c • f) μ
have right : HasFiniteIntegral (c • f) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hf : Integrable f μ
hφ : MemLp φ ∞ μ
⊢ Integrable (φ • f) μ
have rw : ∀ (hf : MemLp f 1 μ) (hφ : MemLp φ ∞ μ), MemLp (φ • f) 1 μ
Tactic: rw [← memLp_one_iff_integrable] at hf ⊢
Cleared hypotheses: hf, hφ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hφ : Integrable φ μ
hf : MemLp f ∞ μ
⊢ Integrable (φ • f) μ
have rw : ∀ (hφ : MemLp φ 1 μ) (hf : MemLp f ∞ μ), MemLp (φ • f) 1 μ
Tactic: rw [← memLp_one_iff_integrable] at hφ ⊢
Cleared hypotheses: hφ, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_9
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
⊢ Integrable.{u_9, u_1} (ε := E) (fun (x : α) ↦ f x • c) μ ↔ Integrable f μ
have simp_rw : AEStronglyMeasurable f μ → (∫⁻ (a : α), ‖f a‖ₑ * ‖c‖ₑ ∂μ < ∞ ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞)
Tactic: simp_rw [Integrable, aestronglyMeasurable_smul_const_iff (f := f) hc, and_congr_right_iff,
    hasFiniteIntegral_iff_enorm, enorm_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_9
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
h : AEStronglyMeasurable f μ
⊢ ∫⁻ (a : α), ‖f a‖ₑ * ‖c‖ₑ ∂μ < ∞ ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
have rw : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞ ∧ ‖c‖ₑ < ∞ ∨ ∫⁻ (a : α), ‖f a‖ₑ ∂μ = 0 ∨ ‖c‖ₑ = 0 ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
Tactic: rw [lintegral_mul_const' _ _ enorm_ne_top, ENNReal.mul_lt_top_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_9
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
h : AEStronglyMeasurable f μ
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞ ∧ ‖c‖ₑ < ∞ ∨ ∫⁻ (a : α), ‖f a‖ₑ ∂μ = 0 ∨ ‖c‖ₑ = 0 ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
have this : ∀ (x : ℝ≥0∞), x = 0 → x < ∞
Tactic: have : ∀ x : ℝ≥0∞, x = 0 → x < ∞ := by simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : NormedDivisionRing 𝕜
f : α → 𝕜
h : Integrable f μ
c : 𝕜
⊢ Integrable.{u_8, u_1} (ε := 𝕜) (fun (x : α) ↦ f x / c) μ
have simp_rw : Integrable.{u_8, u_1} (ε := 𝕜) (fun (x : α) ↦ f x * c⁻¹) μ
Tactic: simp_rw [div_eq_mul_inv, h.mul_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : RCLike 𝕜
f : α → ℝ
hf : Integrable f μ
⊢ Integrable.{u_8, u_1} (ε := 𝕜) (fun (x : α) ↦ (↑(f x) : 𝕜)) μ
have rw : ∀ (hf : MemLp f 1 μ), MemLp.{u_1, u_8} (ε := 𝕜) (fun (x : α) ↦ (↑(f x) : 𝕜)) 1 μ
Tactic: rw [← memLp_one_iff_integrable] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : RCLike 𝕜
f : α → 𝕜
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) μ ∧
      Integrable (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) μ ↔
    Integrable f μ
have simp_rw : MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) 1 μ ∧
    MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) 1 μ ↔
  MemLp f 1 μ
Tactic: simp_rw [← memLp_one_iff_integrable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : RCLike 𝕜
f : α → 𝕜
hf : Integrable f μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) μ
have rw : ∀ (hf : MemLp f 1 μ), MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) 1 μ
Tactic: rw [← memLp_one_iff_integrable] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : RCLike 𝕜
f : α → 𝕜
hf : Integrable f μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) μ
have rw : ∀ (hf : MemLp f 1 μ), MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) 1 μ
Tactic: rw [← memLp_one_iff_integrable] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
⊢ Integrable f (μ'.trim hm)
have refine : HasFiniteIntegral f (μ'.trim hm)
Tactic: refine ⟨hf.aestronglyMeasurable, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
⊢ HasFiniteIntegral f (μ'.trim hm)
have rw : ∫⁻ (a : α), ‖f a‖ₑ ∂μ' < ∞
Tactic: rw [HasFiniteIntegral, lintegral_trim hm _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
rw : ∫⁻ (a : α), ‖f a‖ₑ ∂μ' < ∞
⊢ HasFiniteIntegral f (μ'.trim hm)
have rw₁ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ ‖f a‖ₑ
Tactic: rw [HasFiniteIntegral, lintegral_trim hm _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f (μ'.trim hm)
⊢ Integrable f μ'
have hf_meas_ae : AEStronglyMeasurable f (μ'.trim hm)
Tactic: obtain ⟨hf_meas_ae, hf⟩ := hf_int
Cleared hypotheses: hf_int