mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: case inr
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
t s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
hs : MeasurableSet s
this : ∀ (t : Set G), MeasurableSet t → μ' s * ν' t = ν' s * μ' t
ht : ¬MeasurableSet t
⊢ μ' s * ν' t = ν' s * μ' t

pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
hs : MeasurableSet s
t : Set G
ht : MeasurableSet t
⊢ μ' s * ν' t = ν' s * μ' t

Tactic:
·

Goal state after:
case inr
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
t s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
hs : MeasurableSet s
this : ∀ (t : Set G), MeasurableSet t → μ' s * ν' t = ν' s * μ' t
ht : ¬MeasurableSet t
⊢ μ' s * ν' t = ν' s * μ' t
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case mp.ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}, (fun x ↦ ↑(f x) * g x) x = (fun x ↦ ↑(f' x) * g' x) x

pp: case mp.htc
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}ᶜ, (fun x ↦ ↑(f x) * g x) x = (fun x ↦ ↑(f' x) * g' x) x

Tactic:
·

Goal state after:
case mp.ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}, (fun x ↦ ↑(f x) * g x) x = (fun x ↦ ↑(f' x) * g' x) x
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: case inr
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
t s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
hs : MeasurableSet s
this : ∀ (t : Set G), MeasurableSet t → μ' s * ν' t = ν' s * μ' t
ht : ¬MeasurableSet t
t' : Set G
hm : MeasurableSet t'
hμ : μ' t' = μ' t
hν : ν' t' = ν' t
⊢ μ' s * ν' t' = ν' s * μ' t'

Tactic:
this _ hm

Goal state after:
case inr
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
t s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
hs : MeasurableSet s
this : ∀ (t : Set G), MeasurableSet t → μ' s * ν' t = ν' s * μ' t
ht : ¬MeasurableSet t
t' : Set G
hm : MeasurableSet t'
hμ : μ' t' = μ' t
hν : ν' t' = ν' t
⊢ ν' s * μ' t' = ν' s * μ' t'
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case mp.htc
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}ᶜ, (fun x ↦ ↑(f x) * g x) x = (fun x ↦ ↑(f' x) * g' x) x

Tactic:
·

Goal state after:
case mp.htc
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}ᶜ, (fun x ↦ ↑(f x) * g x) x = (fun x ↦ ↑(f' x) * g' x) x
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
n : ℕ
⊢ μ (s ∩ ⋂ j, notConvergentSeq f g n j) = 0

Tactic:
by
  simp_rw [EMetric.tendsto_atTop, ae_iff] at hfg
  rw [← nonpos_iff_eq_zero, ← hfg]
  refine measure_mono fun x => ?_
  simp only [Set.mem_inter_iff, Set.mem_iInter, mem_notConvergentSeq_iff]
  push Not
  rintro ⟨hmem, hx⟩
  refine ⟨hmem, (n : ℝ≥0∞)⁻¹, by simp, fun N => ?_⟩
  obtain ⟨n, hn₁, hn₂⟩ := hx N
  exact ⟨n, hn₁, hn₂.le⟩

Goal state after:
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
n : ℕ
h : IsEmpty ι
⊢ Tendsto (fun j ↦ μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)

pp: case inr
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
n : ℕ
h : Nonempty ι
⊢ Tendsto (fun j ↦ μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
n : ℕ
h : IsEmpty ι
⊢ Tendsto (fun j ↦ μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case mpr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
⊢ AEMeasurable (fun x ↦ ↑(f x) * g x) μ → AEMeasurable g (μ.withDensity fun x ↦ ↑(f x))

Tactic:
·

Goal state after:
case mpr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
⊢ AEMeasurable (fun x ↦ ↑(f x) * g x) μ → AEMeasurable g (μ.withDensity fun x ↦ ↑(f x))
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case indicator
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s →
      ∫⁻ (a : α), s.indicator (fun x ↦ c) a ∂μ.withDensity f = ∫⁻ (a : α), (f * s.indicator fun x ↦ c) a ∂μ

pp: case add
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ ⦃f_1 g : α → ℝ≥0∞⦄,
    Disjoint (Function.support f_1) (Function.support g) →
      Measurable f_1 →
        Measurable g →
          ∫⁻ (a : α), f_1 a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1) a ∂μ →
            ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ →
              ∫⁻ (a : α), (f_1 + g) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (f_1 + g)) a ∂μ

pp: case iSup
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ ⦃f_1 : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f_1 n)) →
      Monotone f_1 →
        (∀ (n : ℕ), ∫⁻ (a : α), f_1 n a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1 n) a ∂μ) →
          ∫⁻ (a : α), (fun x ↦ ⨆ n, f_1 n x) a ∂μ.withDensity f = ∫⁻ (a : α), (f * fun x ↦ ⨆ n, f_1 n x) a ∂μ

Tactic:
·

Goal state after:
case indicator
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s →
      ∫⁻ (a : α), s.indicator (fun x ↦ c) a ∂μ.withDensity f = ∫⁻ (a : α), (f * s.indicator fun x ↦ c) a ∂μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case add
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ ⦃f_1 g : α → ℝ≥0∞⦄,
    Disjoint (Function.support f_1) (Function.support g) →
      Measurable f_1 →
        Measurable g →
          ∫⁻ (a : α), f_1 a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1) a ∂μ →
            ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ →
              ∫⁻ (a : α), (f_1 + g) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (f_1 + g)) a ∂μ

pp: case iSup
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ ⦃f_1 : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f_1 n)) →
      Monotone f_1 →
        (∀ (n : ℕ), ∫⁻ (a : α), f_1 n a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1 n) a ∂μ) →
          ∫⁻ (a : α), (fun x ↦ ⨆ n, f_1 n x) a ∂μ.withDensity f = ∫⁻ (a : α), (f * fun x ↦ ⨆ n, f_1 n x) a ∂μ

Tactic:
·

Goal state after:
case add
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ ⦃f_1 g : α → ℝ≥0∞⦄,
    Disjoint (Function.support f_1) (Function.support g) →
      Measurable f_1 →
        Measurable g →
          ∫⁻ (a : α), f_1 a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1) a ∂μ →
            ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ →
              ∫⁻ (a : α), (f_1 + g) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (f_1 + g)) a ∂μ
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : a < 0
⊢ b * b - 4 * a * c ≤ 0

pp: case inr.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
b c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c
⊢ b * b - 4 * 0 * c ≤ 0

pp: case inr.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : 0 < a
⊢ b * b - 4 * a * c ≤ 0

Tactic:
·

Goal state after:
case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : a < 0
⊢ b * b - 4 * a * c ≤ 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case iSup
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ ⦃f_1 : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f_1 n)) →
      Monotone f_1 →
        (∀ (n : ℕ), ∫⁻ (a : α), f_1 n a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1 n) a ∂μ) →
          ∫⁻ (a : α), (fun x ↦ ⨆ n, f_1 n x) a ∂μ.withDensity f = ∫⁻ (a : α), (f * fun x ↦ ⨆ n, f_1 n x) a ∂μ

Tactic:
·

Goal state after:
case iSup
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ ⦃f_1 : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f_1 n)) →
      Monotone f_1 →
        (∀ (n : ℕ), ∫⁻ (a : α), f_1 n a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1 n) a ∂μ) →
          ∫⁻ (a : α), (fun x ↦ ⨆ n, f_1 n x) a ∂μ.withDensity f = ∫⁻ (a : α), (f * fun x ↦ ⨆ n, f_1 n x) a ∂μ
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
b c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c
⊢ b * b - 4 * 0 * c ≤ 0

pp: case inr.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : 0 < a
⊢ b * b - 4 * a * c ≤ 0

Tactic:
·

Goal state after:
case inr.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
b c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c
⊢ b * b - 4 * 0 * c ≤ 0
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: case inr.inl.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + 0 * x + c
⊢ 0 * 0 - 4 * 0 * c ≤ 0

pp: case inr.inl.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
b c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c
hb : b ≠ 0
⊢ b * b - 4 * 0 * c ≤ 0

Tactic:
·

Goal state after:
case inr.inl.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + 0 * x + c
⊢ 0 * 0 - 4 * 0 * c ≤ 0
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
hfx : f x = ∞
⊢ ENNReal.ofReal (f x).toReal ≤ f x

pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
hfx : ¬f x = ∞
⊢ ENNReal.ofReal (f x).toReal ≤ f x

Tactic:
·

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
hfx : f x = ∞
⊢ ENNReal.ofReal (f x).toReal ≤ f x
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: case inr.inl.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
b c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c
hb : b ≠ 0
⊢ b * b - 4 * 0 * c ≤ 0

Tactic:
·

Goal state after:
case inr.inl.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
b c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c
hb : b ≠ 0
⊢ b * b - 4 * 0 * c ≤ 0
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
hfx : ¬f x = ∞
⊢ ENNReal.ofReal (f x).toReal ≤ f x

Tactic:
·

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
hfx : ¬f x = ∞
⊢ ENNReal.ofReal (f x).toReal ≤ f x
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: case hf_nonneg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ∀ (n : ℕ), 0 ≤ 2⁻¹ ^ n

pp: case hf
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ Summable (HPow.hPow 2⁻¹)

Tactic:
·

Goal state after:
case hf_nonneg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ∀ (n : ℕ), 0 ≤ 2⁻¹ ^ n
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : 0 < a
⊢ b * b - 4 * a * c ≤ 0

Tactic:
·

Goal state after:
case inr.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : 0 < a
⊢ b * b - 4 * a * c ≤ 0
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ Summable (HPow.hPow 2⁻¹)

Tactic:
·

Goal state after:
case hf
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ Summable (HPow.hPow 2⁻¹)
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this✝ : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
h' : discrim a b c = 0
this : 0 < a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c
⊢ a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c = 0

Tactic:
quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this✝ : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
h' : discrim a b c = 0
this : 0 < a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c
⊢ -b / (2 * a) = -b / (2 * a)
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := ⋯
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := ⋯
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}, (f' * g') x = (f' * g) x

pp: case htc
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := ⋯
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := ⋯
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}ᶜ, (f' * g') x = (f' * g) x

Tactic:
·

Goal state after:
case ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := ⋯
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := ⋯
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}, (f' * g') x = (f' * g) x
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ≥0
⊢ 0 < sqrt x ↔ 0 < x

Tactic:
simp [pos_iff_ne_zero]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case mp
x y : ℝ
⊢ √x = y → y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0

pp: case mpr
x y : ℝ
⊢ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0 → √x = y

Tactic:
·

Goal state after:
case mp
x y : ℝ
⊢ √x = y → y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case mp.inl
x : ℝ
hle : 0 ≤ x
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0

pp: case mp.inr
x : ℝ
hlt : x < 0
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0

Tactic:
·

Goal state after:
case mp.inl
x : ℝ
hle : 0 ≤ x
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case mp.inr
x : ℝ
hlt : x < 0
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0

Tactic:
·

Goal state after:
case mp.inr
x : ℝ
hlt : x < 0
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case mpr
x y : ℝ
⊢ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0 → √x = y

Tactic:
·

Goal state after:
case mpr
x y : ℝ
⊢ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0 → √x = y
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case htc
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := ⋯
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := ⋯
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}ᶜ, (f' * g') x = (f' * g) x

Tactic:
·

Goal state after:
case htc
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := ⋯
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := ⋯
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}ᶜ, (f' * g') x = (f' * g) x
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case mp
x y : ℝ
h : 0 ≤ y
⊢ x ^ 2 ≤ y → -√y ≤ x ∧ x ≤ √y

pp: case mpr
x y : ℝ
h : 0 ≤ y
⊢ -√y ≤ x ∧ x ≤ √y → x ^ 2 ≤ y

Tactic:
·

Goal state after:
case mp
x y : ℝ
h : 0 ≤ y
⊢ x ^ 2 ≤ y → -√y ≤ x ∧ x ≤ √y
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case mpr
x y : ℝ
h : 0 ≤ y
⊢ -√y ≤ x ∧ x ≤ √y → x ^ 2 ≤ y

Tactic:
·

Goal state after:
case mpr
x y : ℝ
h : 0 ≤ y
⊢ -√y ≤ x ∧ x ≤ √y → x ^ 2 ≤ y
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
⊢ HasFiniteIntegral bound μ

pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
⊢ 0 ≤ᵐ[μ] bound

Tactic:
·

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
⊢ HasFiniteIntegral bound μ
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case inl
x y : ℝ
hx : 0 < x
hy : y ≤ 0
⊢ √x ≤ √y ↔ x ≤ y

pp: case inr
x y : ℝ
hx : 0 < x
hy : 0 ≤ y
⊢ √x ≤ √y ↔ x ≤ y

Tactic:
·

Goal state after:
case inl
x y : ℝ
hx : 0 < x
hy : y ≤ 0
⊢ √x ≤ √y ↔ x ≤ y
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case inr
x y : ℝ
hx : 0 < x
hy : 0 ≤ y
⊢ √x ≤ √y ↔ x ≤ y

Tactic:
·

Goal state after:
case inr
x y : ℝ
hx : 0 < x
hy : 0 ≤ y
⊢ √x ≤ √y ↔ x ≤ y
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case inl
x : ℝ
hx : x ≤ 0
⊢ x ≤ √x ↔ x ≤ 1

pp: case inr
x : ℝ
hx : 0 < x
⊢ x ≤ √x ↔ x ≤ 1

Tactic:
·

Goal state after:
case inl
x : ℝ
hx : x ≤ 0
⊢ x ≤ √x ↔ x ≤ 1
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case inr
x : ℝ
hx : 0 < x
⊢ x ≤ √x ↔ x ≤ 1

Tactic:
·

Goal state after:
case inr
x : ℝ
hx : 0 < x
⊢ x ≤ √x ↔ x ≤ 1