awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • (↑r : ℝ)
pos :
  HAdd.hAdd (α := ℝ) (∫ (a : α), max (f a) 0 ∂μ) (∫ (a : α), max (-f a) 0 ∂μ) ≤
    2 * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) * (↑r : ℝ)
⊢ HAdd.hAdd (α := ℝ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ) ≤
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)).toReal

Tactic:
simp only [Real.coe_toNNReal', ENNReal.toReal_mul, ENNReal.coe_toReal,
      toReal_ofNat] at hfint' ⊢

Premises used: ENNReal.coe_toReal, Real.coe_toNNReal', ENNReal.toReal_mul, ENNReal.toReal_ofNat
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) (∫ (a : α), max (-f a) 0 ∂μ) (∫ (a : α), max (f a) 0 ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • (↑r : ℝ)
pos :
  HAdd.hAdd (α := ℝ) (∫ (a : α), max (f a) 0 ∂μ) (∫ (a : α), max (f a) 0 ∂μ) ≤
    2 * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) * (↑r : ℝ)
⊢ HAdd.hAdd (α := ℝ) (∫ (a : α), max (f a) 0 ∂μ) (∫ (a : α), max (-f a) 0 ∂μ) ≤
    2 * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) * (↑r : ℝ)

Tactic:
grw [hfint']
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) (∫ (a : α), max (-f a) 0 ∂μ) (∫ (a : α), max (f a) 0 ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • (↑r : ℝ)
pos : HMul.hMul (α := ℝ) 2 (∫ (a : α), max (f a) 0 ∂μ) ≤ 2 * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) * (↑r : ℝ)
pos₁ :
  HMul.hMul (α := ℝ) 2 (∫ (a : α), max (f a) 0 ∂μ) ≤ 2 * (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) * (↑r : ℝ))
pos₂ pos₃ pos₄ pos₅ : ∫ (a : α), max (f a) 0 ∂μ ≤ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) * (↑r : ℝ)
⊢ HAdd.hAdd (α := ℝ) (∫ (a : α), max (f a) 0 ∂μ) (∫ (a : α), max (f a) 0 ∂μ) ≤
    2 * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) * (↑r : ℝ)

Tactic:
rwa [← two_mul, mul_assoc, mul_le_mul_iff_right₀ (two_pos : (0 : ℝ) < 2)]

Premises used: mul_assoc, two_mul, two_pos, mul_le_mul_iff_right₀
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • (↑r : ℝ)
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ (↑(-f a).toNNReal : ℝ)) μ

Tactic:
hfint.neg.sup (integrable_zero _ _ μ)

Premises used: MeasureTheory.Integrable.sup, MeasureTheory.Integrable.neg, MeasureTheory.integrable_zero, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • (↑r : ℝ)
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ (↑(-f a).toNNReal : ℝ)) μ

Tactic:
exact hfint.neg.sup (integrable_zero _ _ μ)

Premises used: MeasureTheory.Integrable.sup, MeasureTheory.Integrable.neg, MeasureTheory.integrable_zero
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ r
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * ENNReal.ofReal r

Tactic:
eLpNorm_one_le_of_le hfint hfint' ?_

Premises used: ENNReal.ofReal, MeasureTheory.eLpNorm_one_le_of_le
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ r
refine : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r.toNNReal : ℝ)
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * ENNReal.ofReal r

Tactic:
refine eLpNorm_one_le_of_le hfint hfint' ?_

Premises used: MeasureTheory.eLpNorm_one_le_of_le
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ r
simp : ∀ᵐ (ω : α) ∂μ, f ω ≤ r ∨ f ω ≤ 0
⊢ ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r.toNNReal : ℝ)

Tactic:
simp only [Real.coe_toNNReal', le_max_iff]

Premises used: Real.coe_toNNReal', le_max_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ r
ω : α
hω : f ω ≤ r
⊢ f ω ≤ r ∨ f ω ≤ 0

Tactic:
Or.inl hω

Premises used: Or.inl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ r
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (ω : α) ↦ f ω ≤ r) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (ω : α) ↦ f ω ≤ r ∨ f ω ≤ 0) x} x}
      a
h₁ h₂ : ∀ (ω : α) (hω : f ω ≤ r), f ω ≤ r ∨ f ω ≤ 0
⊢ ∀ᵐ (ω : α) ∂μ, f ω ≤ r ∨ f ω ≤ 0

Tactic:
filter_upwards [hf] with ω hω using Or.inl hω
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
p : ℝ≥0∞
inst_7 : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
L : E →SL[σ] F
φ : ↥(Lp E p μ)
⊢ Eq.{u_4 + 1} (α := F)
    (∫ (x : X), (↑(↑(compLp.{u_1, u_3, u_4, u_6, u_7} (𝕜 := 𝕜) (𝕜' := 𝕜') (σ := σ) L φ) : X →ₘ[μ] F) : X → F) x ∂μ)
    (∫ (x : X), (L : (a : E) → F) ((↑(↑φ : X →ₘ[μ] E) : X → E) x) ∂μ)

Tactic:
integral_congr_ae <| coeFn_compLp _ _

Premises used: MeasureTheory.integral_congr_ae, ContinuousLinearMap.coeFn_compLp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
p : ℝ≥0∞
inst_7 : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
L : E →SL[σ] F
φ : ↥(Lp E p μ)
s : Set X
hs : MeasurableSet s
⊢ Eq.{u_4 + 1} (α := F)
    (∫ (x : X) in s, (↑(↑(compLp.{u_1, u_3, u_4, u_6, u_7} (𝕜 := 𝕜) (𝕜' := 𝕜') (σ := σ) L φ) : X →ₘ[μ] F) : X → F) x ∂μ)
    (∫ (x : X) in s, (L : (a : E) → F) ((↑(↑φ : X →ₘ[μ] E) : X → E) x) ∂μ)

Tactic:
setIntegral_congr_ae hs ((L.coeFn_compLp φ).mono fun _x hx _ => hx)

Premises used: MeasureTheory.setIntegral_congr_ae, Filter.Eventually.mono, ContinuousLinearMap.coeFn_compLp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
L : E →SL[σ] F
rw :
  Continuous (Y := F) fun (x : ↥(Lp E 1 μ)) ↦
    ∫ (x_1 : X), (↑(↑(compLp.{u_1, u_3, u_4, u_6, u_7} (𝕜 := 𝕜) (𝕜' := 𝕜') (σ := σ) L x) : X →ₘ[μ] F) : X → F) x_1 ∂μ
⊢ Continuous (Y := F) fun (φ : ↥(Lp E 1 μ)) ↦ ∫ (x : X), (L : (a : E) → F) ((↑(↑φ : X →ₘ[μ] E) : X → E) x) ∂μ

Tactic:
rw [← funext L.integral_compLp]

Premises used: ContinuousLinearMap.integral_compLp, funext
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
L : E →SL[σ] F
⊢ Continuous (Y := F) fun (x : ↥(Lp E 1 μ)) ↦
    ∫ (x_1 : X), (↑(↑(compLp.{u_1, u_3, u_4, u_6, u_7} (𝕜 := 𝕜) (𝕜' := 𝕜') (σ := σ) L x) : X →ₘ[μ] F) : X → F) x_1 ∂μ

Tactic:
continuous_integral.comp (L.compLpL 1 μ).continuous

Premises used: Continuous.comp, ContinuousLinearMap.continuous, MeasureTheory.continuous_integral, ContinuousLinearMap.compLpL, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
L : E →SL[σ] F
⊢ Continuous (Y := F) fun (x : ↥(Lp E 1 μ)) ↦
    ∫ (x_1 : X), (↑(↑(compLp.{u_1, u_3, u_4, u_6, u_7} (𝕜 := 𝕜) (𝕜' := 𝕜') (σ := σ) L x) : X →ₘ[μ] F) : X → F) x_1 ∂μ

Tactic:
exact continuous_integral.comp (L.compLpL 1 μ).continuous

Premises used: Continuous.comp, ContinuousLinearMap.continuous, MeasureTheory.continuous_integral, ContinuousLinearMap.compLpL, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
inst_9 : CompleteSpace F
inst_10 : NormedSpace ℝ E
inst_11 : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), (σ : (a : 𝕜) → 𝕜') (r • x) = HSMul.hSMul (β := 𝕜') r ((σ : (a : 𝕜) → 𝕜') x : 𝕜')
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
h_ind :
  ∀ (c : E) ⦃s : Set X⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        (fun (φ : X → E) ↦
            Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F)
              ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
          (s.indicator fun (x : X) ↦ c)
h_add :
  ∀ ⦃f g : X → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      Integrable f μ →
        Integrable g μ →
          (fun (φ : X → E) ↦
                Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F)
                  ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
              f →
            (fun (φ : X → E) ↦
                  Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F)
                    ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
                g →
              (fun (φ : X → E) ↦
                  Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F)
                    ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
                (f + g)
h_closed :
  IsClosed (X := ↥(Lp E 1 μ))
    {f : ↥(Lp E 1 μ) |
      (fun (φ : X → E) ↦
          Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
        (↑(↑f : X →ₘ[μ] E) : X → E)}
h_ae :
  ∀ ⦃f g : X → E⦄,
    f =ᶠ[ae μ] g →
      Integrable f μ →
        (fun (φ : X → E) ↦
              Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F)
                ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
            f →
          (fun (φ : X → E) ↦
              Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F)
                ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
            g
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F)

Tactic:
apply φ_int.induction (P := fun φ => ∫ x, L (φ x) ∂μ = L (∫ x, φ x ∂μ))

Premises used: MeasureTheory.integral, Eq, DFunLike.coe, MeasureTheory.Integrable.induction
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
inst_9 : CompleteSpace F
inst_10 : NormedSpace ℝ E
inst_11 : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), (σ : (a : 𝕜) → 𝕜') (r • x) = HSMul.hSMul (β := 𝕜') r ((σ : (a : 𝕜) → 𝕜') x : 𝕜')
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
e : E
s : Set X
s_meas : MeasurableSet s
h_ind :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) x) ∂μ : F)
      ((L : (a : E) → F) (∫ (x : X), s.indicator (fun (x : X) ↦ e) x ∂μ) : F)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
    (fun (φ : X → E) ↦
        Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
      (s.indicator fun (x : X) ↦ e)

Tactic:
_
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
inst_9 : CompleteSpace F
inst_10 : NormedSpace ℝ E
inst_11 : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), (σ : (a : 𝕜) → 𝕜') (r • x) = HSMul.hSMul (β := 𝕜') r ((σ : (a : 𝕜) → 𝕜') x : 𝕜')
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
e : E
s : Set X
s_meas : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_ind :
  Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) x) ∂μ)
    (∫ (x : X), s.indicator (fun (x : X) ↦ (L : (a : E) → F) e) x ∂μ)
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) x) ∂μ : F)
    ((L : (a : E) → F) (∫ (x : X), s.indicator (fun (x : X) ↦ e) x ∂μ) : F)

Tactic:
rw [integral_indicator_const e s_meas, ← @smul_one_smul E ℝ 𝕜 _ _ _ _ _ (μ.real s) e,
      map_smulₛₗ, hσ, map_one, smul_assoc, one_smul,
      ← integral_indicator_const (L e) s_meas]

Premises used: smul_assoc, MeasureTheory.Measure.real, MulActionSemiHomClass.map_smulₛₗ, one_smul, smul_one_smul, map_one, MeasureTheory.integral_indicator_const, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
inst_9 : CompleteSpace F
inst_10 : NormedSpace ℝ E
inst_11 : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), (σ : (a : 𝕜) → 𝕜') (r • x) = HSMul.hSMul (β := 𝕜') r ((σ : (a : 𝕜) → 𝕜') x : 𝕜')
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
e : E
s : Set X
s_meas : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_ind :
  ∀ (a : X),
    Eq.{u_4 + 1} (α := F) ((L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) a) : F)
      (s.indicator (fun (x : X) ↦ (L : (a : E) → F) e) a : F)
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) x) ∂μ)
    (∫ (x : X), s.indicator (fun (x : X) ↦ (L : (a : E) → F) e) x ∂μ)

Tactic:
congr 1 with a
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
inst_9 : CompleteSpace F
inst_10 : NormedSpace ℝ E
inst_11 : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), (σ : (a : 𝕜) → 𝕜') (r • x) = HSMul.hSMul (β := 𝕜') r ((σ : (a : 𝕜) → 𝕜') x : 𝕜')
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
e : E
s : Set X
s_meas : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
a : X
h_ind :
  Eq.{u_4 + 1} (α := F) ((L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) a) : F)
    (s.indicator (Function.comp.{u_1 + 1, u_3 + 1, u_4 + 1} (β := E) (⇑L : (a : E) → F) fun (x : X) ↦ e) a : F)
h_ind₁ :
  Eq.{u_4 + 1} (α := F) ((L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) a) : F)
    (Function.comp.{u_1 + 1, u_3 + 1, u_4 + 1} (β := E) (⇑L : (a : E) → F) (s.indicator fun (x : X) ↦ e) a : F)
h_ind₂ h_ind₃ :
  Eq.{u_4 + 1} (α := F) ((L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) a) : F)
    ((L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) a) : F)
⊢ Eq.{u_4 + 1} (α := F) ((L : (a : E) → F) (s.indicator (fun (x : X) ↦ e) a) : F)
    (s.indicator (fun (x : X) ↦ (L : (a : E) → F) e) a : F)

Tactic:
rw [← Function.comp_def L, Set.indicator_comp_of_zero L.map_zero, Function.comp_apply]

Premises used: ContinuousLinearMap.map_zero, Function.comp_def, Set.indicator_comp_of_zero, Function.comp_apply, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
inst_9 : CompleteSpace F
inst_10 : NormedSpace ℝ E
inst_11 : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), (σ : (a : 𝕜) → 𝕜') (r • x) = HSMul.hSMul (β := 𝕜') r ((σ : (a : 𝕜) → 𝕜') x : 𝕜')
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
f g : X → E
h_add :
  Disjoint (Function.support f) (Function.support g) →
    Integrable f μ →
      Integrable g μ →
        (fun (φ : X → E) ↦
              Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F)
                ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
            f →
          (fun (φ : X → E) ↦
                Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F)
                  ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
              g →
            (fun (φ : X → E) ↦
                Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F)
                  ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
              (f + g)
⊢ Disjoint (Function.support f) (Function.support g) →
    Integrable f μ →
      Integrable g μ →
        (fun (φ : X → E) ↦
              Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F)
                ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
            f →
          (fun (φ : X → E) ↦
                Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F)
                  ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
              g →
            (fun (φ : X → E) ↦
                Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F)
                  ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
              (f + g)

Tactic:
_
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
inst_9 : CompleteSpace F
inst_10 : NormedSpace ℝ E
inst_11 : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), (σ : (a : 𝕜) → 𝕜') (r • x) = HSMul.hSMul (β := 𝕜') r ((σ : (a : 𝕜) → 𝕜') x : 𝕜')
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
f g : X → E
h : Disjoint (Function.support f) (Function.support g)
f_int : Integrable f μ
g_int : Integrable g μ
hf : Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (f x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), f x ∂μ) : F)
hg : Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (g x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), g x ∂μ) : F)
⊢ Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) ((f + g) x) ∂μ : F)
    ((L : (a : E) → F) (∫ (x : X), (f + g) x ∂μ) : F)

Tactic:
simp [L.map_add, integral_add (μ := μ) f_int g_int,
      integral_add (μ := μ) (L.integrable_comp f_int) (L.integrable_comp g_int), hf, hg]

Premises used: ContinuousLinearMap.integrable_comp, ContinuousLinearMap.map_add, MeasureTheory.integral_add
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
inst_9 : CompleteSpace F
inst_10 : NormedSpace ℝ E
inst_11 : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), (σ : (a : 𝕜) → 𝕜') (r • x) = HSMul.hSMul (β := 𝕜') r ((σ : (a : 𝕜) → 𝕜') x : 𝕜')
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
⊢ IsClosed (X := ↥(Lp E 1 μ))
    {f : ↥(Lp E 1 μ) |
      (fun (φ : X → E) ↦
          Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
        (↑(↑f : X →ₘ[μ] E) : X → E)}

Tactic:
isClosed_eq L.continuous_integral_comp_L1 (L.continuous.comp continuous_integral)

Premises used: ContinuousLinearMap.continuous_integral_comp_L1, Continuous.comp, setOf, ContinuousLinearMap.continuous, isClosed_eq, MeasureTheory.continuous_integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
inst_9 : CompleteSpace F
inst_10 : NormedSpace ℝ E
inst_11 : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), (σ : (a : 𝕜) → 𝕜') (r • x) = HSMul.hSMul (β := 𝕜') r ((σ : (a : 𝕜) → 𝕜') x : 𝕜')
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
⊢ IsClosed (X := ↥(Lp E 1 μ))
    {f : ↥(Lp E 1 μ) |
      (fun (φ : X → E) ↦
          Eq.{u_4 + 1} (α := F) (∫ (x : X), (L : (a : E) → F) (φ x) ∂μ : F) ((L : (a : E) → F) (∫ (x : X), φ x ∂μ) : F))
        (↑(↑f : X →ₘ[μ] E) : X → E)}

Tactic:
exact isClosed_eq L.continuous_integral_comp_L1 (L.continuous.comp continuous_integral)

Premises used: ContinuousLinearMap.continuous_integral_comp_L1, Continuous.comp, ContinuousLinearMap.continuous, isClosed_eq, MeasureTheory.continuous_integral