awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
rw : (eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ).toReal ≤ ‖c‖ * μ.real s ^ (1 / p.toReal)
⊢ norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) ≤ ‖c‖ * μ.real s ^ (1 / p.toReal)

Tactic:
rw [indicatorConstLp, Lp.norm_toLp]

Premises used: MeasureTheory.indicatorConstLp, MeasureTheory.Lp.norm_toLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
⊢ 0 ≤ ‖c‖ * μ.real s ^ (1 / p.toReal)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
refine :
  eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ENNReal.ofReal (‖c‖ * μ.real s ^ (1 / p.toReal))
⊢ (eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ).toReal ≤ ‖c‖ * μ.real s ^ (1 / p.toReal)

Tactic:
refine ENNReal.toReal_le_of_le_ofReal (by positivity) ?_

Premises used: ENNReal.toReal_le_of_le_ofReal
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
⊢ eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ENNReal.ofReal (‖c‖ * μ.real s ^ (1 / p.toReal))

Tactic:
(eLpNorm_indicator_const_le _ _).trans_eq ?_

Premises used: LE.le.trans_eq, MeasureTheory.eLpNorm_indicator_const_le
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
refine :
  ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) =
    ENNReal.ofReal (‖c‖ * μ.real s ^ (1 / p.toReal))
⊢ eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (x : α) ↦ c) p μ ≤ ENNReal.ofReal (‖c‖ * μ.real s ^ (1 / p.toReal))

Tactic:
refine (eLpNorm_indicator_const_le _ _).trans_eq ?_

Premises used: LE.le.trans_eq, MeasureTheory.eLpNorm_indicator_const_le
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
rw : HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≠ ∞
⊢ ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) =
    ENNReal.ofReal (‖c‖ * μ.real s ^ (1 / p.toReal))

Tactic:
rw [ENNReal.ofReal_mul (norm_nonneg _), ofReal_norm, measureReal_def,
    ENNReal.toReal_rpow, ENNReal.ofReal_toReal]

Premises used: ENNReal.ofReal_mul, ENNReal.ofReal_toReal, MeasureTheory.measureReal_def, ENNReal.toReal_rpow, ofReal_norm, norm_nonneg
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
⊢ HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
⊢ nnnorm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) ≤
    ‖c‖₊ * ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s) ^ (1 / p.toReal)

Tactic:
norm_indicatorConstLp_le

Premises used: MeasureTheory.norm_indicatorConstLp_le, MeasureTheory.Measure.real, ENNReal.toReal
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
⊢ enorm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) ≤
    ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)

Tactic:
simpa [ENNReal.coe_rpow_of_nonneg, ENNReal.coe_toNNReal hμs, Lp.enorm_def, ← enorm_eq_nnnorm]
    using ENNReal.coe_le_coe.2 <| nnnorm_indicatorConstLp_le (c := c) (hμs := hμs)

Premises used: ENNReal.coe_toNNReal, Iff.mpr, ENNReal.coe_rpow_of_nonneg, ENNReal.coe_le_coe, enorm_eq_nnnorm, MeasureTheory.nnnorm_indicatorConstLp_le, MeasureTheory.Lp.enorm_def
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
unfold :
  edist (α := ↥(Lp E p μ)) (MemLp.toLp (s.indicator fun (x : α) ↦ c) ⋯) (MemLp.toLp (t.indicator fun (x : α) ↦ c) ⋯) =
    enorm (E := ↥(Lp E p μ)) (MemLp.toLp ((s ∆ t).indicator fun (x : α) ↦ c) ⋯)
⊢ edist (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) (indicatorConstLp (s := t) p ht hμt c) =
    enorm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s ∆ t) p ⋯ ⋯ c)

Tactic:
unfold indicatorConstLp

Premises used: MeasureTheory.indicatorConstLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  eLpNorm (HSub.hSub (α := α → E) (s.indicator fun (x : α) ↦ c) (t.indicator fun (x : α) ↦ c)) p μ =
    enorm (E := ↥(Lp E p μ)) (MemLp.toLp ((s ∆ t).indicator fun (x : α) ↦ c) ⋯)
rw₁ :
  eLpNorm.{u_1, u_2} (ε := E) ((s ∆ t).indicator fun (x : α) ↦ c) p μ =
    enorm (E := ↥(Lp E p μ)) (MemLp.toLp ((s ∆ t).indicator fun (x : α) ↦ c) ⋯)
rw₂ rw₃ :
  eLpNorm.{u_1, u_2} (ε := E) ((s ∆ t).indicator fun (x : α) ↦ c) p μ =
    eLpNorm.{u_1, u_2} (ε := E) ((s ∆ t).indicator fun (x : α) ↦ c) p μ
⊢ edist (α := ↥(Lp E p μ)) (MemLp.toLp (s.indicator fun (x : α) ↦ c) ⋯) (MemLp.toLp (t.indicator fun (x : α) ↦ c) ⋯) =
    enorm (E := ↥(Lp E p μ)) (MemLp.toLp ((s ∆ t).indicator fun (x : α) ↦ c) ⋯)

Tactic:
rw [Lp.edist_toLp_toLp, eLpNorm_indicator_sub_indicator, Lp.enorm_toLp]

Premises used: MeasureTheory.Lp.enorm_toLp, MeasureTheory.Lp.edist_toLp_toLp, MeasureTheory.eLpNorm_indicator_sub_indicator
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ dist (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) (indicatorConstLp (s := t) p ht hμt c) =
    norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s ∆ t) p ⋯ ⋯ c)

Tactic:
simp only [Lp.dist_edist, edist_indicatorConstLp_eq_enorm, enorm, ENNReal.coe_toReal,
    Lp.coe_nnnorm]

Premises used: ENNReal.coe_toReal, MeasureTheory.Lp.dist_edist, MeasureTheory.edist_indicatorConstLp_eq_enorm, MeasureTheory.Lp.coe_nnnorm, ENorm.enorm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp₁ : Fact (1 ≤ p)
β : Type u_3
l : Filter β
t : β → Set α
ht : ∀ (b : β), MeasurableSet (t b)
hμt : ∀ (b : β), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t b) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp : p ≠ ∞
h : Tendsto (β := ℝ≥0∞) (fun (b : β) ↦ (μ : (a : Set α) → ℝ≥0∞) (t b ∆ s)) l (𝓝 0)
rw :
  Tendsto (β := ℝ)
    (fun (b : β) ↦ dist (α := ↥(Lp E p μ)) (indicatorConstLp (s := t b) p ⋯ ⋯ c) (indicatorConstLp (s := s) p hs hμs c))
    l (𝓝 0)
⊢ Tendsto (β := ↥(Lp E p μ)) (fun (b : β) ↦ indicatorConstLp (s := t b) p ⋯ ⋯ c) l
    (𝓝 (indicatorConstLp (s := s) p hs hμs c))

Tactic:
rw [tendsto_iff_dist_tendsto_zero]

Premises used: tendsto_iff_dist_tendsto_zero
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp₁ : Fact (1 ≤ p)
β : Type u_3
l : Filter β
t : β → Set α
ht : ∀ (b : β), MeasurableSet (t b)
hμt : ∀ (b : β), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t b) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp : p ≠ ∞
h : Tendsto (β := ℝ≥0∞) (fun (b : β) ↦ (μ : (a : Set α) → ℝ≥0∞) (t b ∆ s)) l (𝓝 0)
⊢ p ≠ 0

Tactic:
have hp₀ : p ≠ 0 := (one_pos.trans_le hp₁.out).ne'
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp₁ : Fact (1 ≤ p)
β : Type u_3
l : Filter β
t : β → Set α
ht : ∀ (b : β), MeasurableSet (t b)
hμt : ∀ (b : β), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t b) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp : p ≠ ∞
h : Tendsto (β := ℝ≥0∞) (fun (b : β) ↦ (μ : (a : Set α) → ℝ≥0∞) (t b ∆ s)) l (𝓝 0)
hp₀ : p ≠ 0
simp : Tendsto (β := ℝ) (fun (b : β) ↦ ‖c‖ * μ.real (t b ∆ s) ^ (1 / p.toReal)) l (𝓝 0)
⊢ Tendsto (β := ℝ)
    (fun (b : β) ↦ dist (α := ↥(Lp E p μ)) (indicatorConstLp (s := t b) p ⋯ ⋯ c) (indicatorConstLp (s := s) p hs hμs c))
    l (𝓝 0)

Tactic:
simp only [dist_indicatorConstLp_eq_norm, norm_indicatorConstLp hp₀ hp]

Premises used: MeasureTheory.norm_indicatorConstLp, MeasureTheory.dist_indicatorConstLp_eq_norm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp₁ : Fact (1 ≤ p)
β : Type u_3
l : Filter β
t : β → Set α
ht : ∀ (b : β), MeasurableSet (t b)
hμt : ∀ (b : β), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t b) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp : p ≠ ∞
h : Tendsto (β := ℝ≥0∞) (fun (b : β) ↦ (μ : (a : Set α) → ℝ≥0∞) (t b ∆ s)) l (𝓝 0)
hp₀ : p ≠ 0
⊢ Tendsto (fun (x : β) ↦ ‖c‖ * (ENNReal.toReal ∘ fun (b : β) ↦ (μ : (a : Set α) → ℝ≥0∞) (t b ∆ s)) x ^ (1 / p.toReal)) l
    (𝓝 (‖c‖ * ENNReal.toReal 0 ^ (1 / p.toReal)))

Tactic:
tendsto_const_nhds.mul (((ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp h).rpow_const _)

Premises used: tendsto_const_nhds, ENNReal.tendsto_toReal, ENNReal.zero_ne_top, Filter.Tendsto.rpow_const, Filter.Tendsto.mul, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp₁ : Fact (1 ≤ p)
β : Type u_3
l : Filter β
t : β → Set α
ht : ∀ (b : β), MeasurableSet (t b)
hμt : ∀ (b : β), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t b) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp : p ≠ ∞
h : Tendsto (β := ℝ≥0∞) (fun (b : β) ↦ (μ : (a : Set α) → ℝ≥0∞) (t b ∆ s)) l (𝓝 0)
hp₀ : p ≠ 0
h₁ : 0 = ‖c‖ * ENNReal.toReal 0 ^ (1 / p.toReal)
convert_3 : ENNReal.toReal 0 ≠ 0 ∨ 0 ≤ 1 / p.toReal
⊢ Tendsto (β := ℝ) (fun (b : β) ↦ ‖c‖ * μ.real (t b ∆ s) ^ (1 / p.toReal)) l (𝓝 0)

Tactic:
convert!
    tendsto_const_nhds.mul (((ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp h).rpow_const _)

Premises used: tendsto_const_nhds, ENNReal.tendsto_toReal, ENNReal.zero_ne_top, Filter.Tendsto.rpow_const, Filter.Tendsto.mul, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp₁ : Fact (1 ≤ p)
β : Type u_3
l : Filter β
t : β → Set α
ht : ∀ (b : β), MeasurableSet (t b)
hμt : ∀ (b : β), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t b) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp : p ≠ ∞
h : Tendsto (β := ℝ≥0∞) (fun (b : β) ↦ (μ : (a : Set α) → ℝ≥0∞) (t b ∆ s)) l (𝓝 0)
hp₀ : p ≠ 0
⊢ 0 = ‖c‖ * ENNReal.toReal 0 ^ (1 / p.toReal)

Tactic:
simp [ENNReal.toReal_eq_zero_iff, hp, hp₀]

Premises used: ENNReal.toReal_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp₁ : Fact (1 ≤ p)
β : Type u_3
l : Filter β
t : β → Set α
ht : ∀ (b : β), MeasurableSet (t b)
hμt : ∀ (b : β), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t b) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp : p ≠ ∞
h : Tendsto (β := ℝ≥0∞) (fun (b : β) ↦ (μ : (a : Set α) → ℝ≥0∞) (t b ∆ s)) l (𝓝 0)
hp₀ : p ≠ 0
⊢ ENNReal.toReal 0 ≠ 0 ∨ 0 ≤ 1 / p.toReal

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
c : E
inst_1 : Fact (1 ≤ p)
X : Type u_3
inst_2 : TopologicalSpace X
s : X → Set α
hs : ∀ (x : X), MeasurableSet (s x)
hμs : ∀ (x : X), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s x) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp : p ≠ ∞
h : ∀ (x : X), Tendsto (β := ℝ≥0∞) (fun (y : X) ↦ (μ : (a : Set α) → ℝ≥0∞) (s y ∆ s x)) (𝓝 x) (𝓝 0)
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    indicatorConstLp (s := s x) p ⋯ ⋯ c

Tactic:
continuous_iff_continuousAt.2 fun x ↦ tendsto_indicatorConstLp_set hp (h x)

Premises used: Iff.mpr, MeasureTheory.tendsto_indicatorConstLp_set, continuous_iff_continuousAt
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
c : E
⊢ Eq (α := ↥(Lp E p μ)) (indicatorConstLp (s := ∅) p ⋯ ⋯ c) 0

Tactic:
simp only [indicatorConstLp, Set.indicator_empty', MemLp.toLp_zero]

Premises used: MeasureTheory.indicatorConstLp, Set.indicator_empty', MeasureTheory.MemLp.toLp_zero
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s t : Set α
hs : MeasurableSet s
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hc : c ≠ 0
simp_rw :
  Eq (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hsμ c) (indicatorConstLp (s := t) p ht htμ c) ↔
    EventuallyEq.{u_1, u_2} (β := E) (ae μ) (s.indicator fun (x : α) ↦ c) (t.indicator fun (x : α) ↦ c)
simp_rw₁ :
  Eq (α := ↥(Lp E p μ)) (MemLp.toLp (s.indicator fun (x : α) ↦ c) ⋯) (MemLp.toLp (t.indicator fun (x : α) ↦ c) ⋯) ↔
    EventuallyEq.{u_1, u_2} (β := E) (ae μ) (s.indicator fun (x : α) ↦ c) (t.indicator fun (x : α) ↦ c)
⊢ Eq (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hsμ c) (indicatorConstLp (s := t) p ht htμ c) ↔ s =ᶠ[ae μ] t

Tactic:
simp_rw [← indicator_const_eventuallyEq hc, indicatorConstLp, MemLp.toLp_eq_toLp_iff]

Premises used: MeasureTheory.MemLp.toLp_eq_toLp_iff, Filter.indicator_const_eventuallyEq, MeasureTheory.indicatorConstLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ MemLp (f + g) p μ ↔ MemLp f p μ ∧ MemLp g p μ

Tactic:
⟨fun hfg => ⟨?_, ?_⟩, fun h => h.1.add h.2⟩

Premises used: MeasureTheory.MemLp.add, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
refine_1 : ∀ (hfg : MemLp (f + g) p μ), MemLp f p μ
refine_2 : ∀ (hfg : MemLp (f + g) p μ), MemLp g p μ
⊢ MemLp (f + g) p μ ↔ MemLp f p μ ∧ MemLp g p μ

Tactic:
refine ⟨fun hfg => ⟨?_, ?_⟩, fun h => h.1.add h.2⟩
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
hfg : MemLp (f + g) p μ
refine_1 : MemLp ((support f).indicator (f + g)) p μ
⊢ MemLp f p μ

Tactic:
rw [← Set.indicator_add_eq_left h]

Premises used: Set.indicator_add_eq_left
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp ((support f).indicator (f + g)) p μ

Tactic:
hfg.indicator (measurableSet_support hf.measurable)

Premises used: measurableSet_support, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.MemLp.indicator
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp ((support f).indicator (f + g)) p μ

Tactic:
exact hfg.indicator (measurableSet_support hf.measurable)

Premises used: measurableSet_support, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.MemLp.indicator
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
hfg : MemLp (f + g) p μ
refine_2 : MemLp ((support g).indicator (f + g)) p μ
⊢ MemLp g p μ

Tactic:
rw [← Set.indicator_add_eq_right h]

Premises used: Set.indicator_add_eq_right
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp ((support g).indicator (f + g)) p μ

Tactic:
hfg.indicator (measurableSet_support hg.measurable)

Premises used: measurableSet_support, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.MemLp.indicator
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp ((support g).indicator (f + g)) p μ

Tactic:
exact hfg.indicator (measurableSet_support hg.measurable)

Premises used: measurableSet_support, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.MemLp.indicator
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s_1 : Set α
hs_1 : MeasurableSet s_1
hμs_1 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
c_1 : E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
c : E
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
c : E
h :
  (↑(↑(indicatorConstLp (s := s ∪ t) p ⋯ ⋯ c) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    (↑(↑(HAdd.hAdd (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) (indicatorConstLp (s := t) p ht hμt c)) :
          α →ₘ[μ] E) :
      α → E)
⊢ indicatorConstLp (s := s ∪ t) p ⋯ ⋯ c =
    HAdd.hAdd (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) (indicatorConstLp (s := t) p ht hμt c)

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
c : E
h :
  ((s ∪ t).indicator fun (x : α) ↦ c) =ᶠ[ae μ]
    HAdd.hAdd (α := α → E) (s.indicator fun (x : α) ↦ c) (t.indicator fun (x : α) ↦ c)
⊢ (↑(↑(indicatorConstLp (s := s ∪ t) p ⋯ ⋯ c) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    (↑(↑(HAdd.hAdd (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) (indicatorConstLp (s := t) p ht hμt c)) :
          α →ₘ[μ] E) :
      α → E)

Tactic:
grw [Lp.coeFn_add, indicatorConstLp_coeFn, indicatorConstLp_coeFn, indicatorConstLp_coeFn]

Premises used: MeasureTheory.Lp.coeFn_add, MeasureTheory.indicatorConstLp_coeFn