mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
⊢ ∃ u ⊆ t, u.Countable ∧ u.PairwiseDisjoint B ∧ μ (s \ ⋃ a ∈ u, B a) = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
⊢ (r • μ).singularPart ν = r • μ.singularPart ν

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
⊢ μ.singularPart (r • ν) = μ.singularPart ν

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
d_Inter :
  ∀ (s : ℕ → Set α),
    (∀ (n : ℕ), MeasurableSet (s n)) →
      (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋂ n, s n)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun n m ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ}, a ≤ b → c ≤ d → f a d ⊆ f b c
f_succ : ∀ (n m : ℕ), n ≤ m → f n (m + 1) = f n m ∩ e (m + 1)
le_d_f : ∀ (n m : ℕ), m ≤ n → γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
s : Set α := ⋃ m, ⋂ n, f m n
γ_le_d_s : γ ≤ d s
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ sᶜ
⊢ d (s ∪ t) ≤ γ + 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (fun i ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (fun i ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I : ∀ᶠ (i : ι) in l, ∫ (y : α), g i y • (f y - c) ∂μ + (∫ (y : α), g i y ∂μ) • c = ∫ (y : α), g i y • f y ∂μ
this✝ : Tendsto (fun x ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
h''i : IntegrableOn f (a i) μ
hi_int : 0 < ∫ (y : α), g i y ∂μ
mu_ai : μ (a i) < ∞
this : ∀ x ∉ a i, ‖g i x‖ * ‖f x - c‖ = 0
x : α
⊢ 0 x ≤ (fun x ↦ ‖g i x‖ * ‖f x - c‖) x

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst✝¹ : μ₁.HaveLebesgueDecomposition ν
inst✝ : μ₂.HaveLebesgueDecomposition ν
⊢ (μ₁ + μ₂).singularPart ν = μ₁.singularPart ν + μ₂.singularPart ν

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
x : α
hf : ∀ (U : Set ℝ), 0 ∈ U → IsOpen U → ∃ y ∈ U, (∃ a ∈ t, r a = y ∧ c a = x) ∧ y ∈ Ioi 0
hx : x ∈ s
ε : ℝ
hε : ε > 0
⊢ 0 ∈ Ioo (-ε) ε

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
⊢ (μ.restrict s).singularPart ν = (μ.singularPart ν).restrict s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
x : α
hf : ∀ (U : Set ℝ), 0 ∈ U → IsOpen U → ∃ y ∈ U, (∃ a ∈ t, r a = y ∧ c a = x) ∧ y ∈ Ioi 0
hx : x ∈ s
ε : ℝ
hε : ε > 0
w✝ : ℝ
left✝ : w✝ ∈ Ioo (-ε) ε
right✝ : w✝ ∈ Ioi 0
a : ι
ha₁ : a ∈ t
ha₂ : r a = w✝
ha₃ : c a = x
⊢ r a ≤ ε

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : μ.HaveLebesgueDecomposition ν
hμs : (μ.singularPart ν) sᶜ = 0
hνs : (ν.withDensity (μ.rnDeriv ν)) s = 0
⊢ μ.singularPart ν = μ.restrict s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∃ᶠ (ε : ℝ) in 𝓝[>] 0, ∃ a ∈ t, r a = ε ∧ c a = x
⊢ ∃ u ⊆ t, u.Countable ∧ u.PairwiseDisjoint B ∧ μ (s \ ⋃ a ∈ u, B a) = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∃ᶠ (ε : ℝ) in 𝓝[>] 0, ∃ a ∈ t, r a = ε ∧ c a = x
⊢ ∃ u ⊆ t, u.Countable ∧ u.PairwiseDisjoint B ∧ μ (s \ ⋃ a ∈ u, B a) = 0

Tactic:
by
  suffices ∀ x ∈ s, ∀ ε > (0 : ℝ), ∃ a ∈ t, r a ≤ ε ∧ c a = x from
    exists_disjoint_covering_ae μ s t C r c B hB μB ht h't this
  intro x hx ε hε
  specialize hf x hx
  rw [frequently_nhdsWithin_iff, frequently_nhds_iff] at hf
  obtain ⟨_, _, ⟨a, ha₁, ha₂, ha₃⟩, _⟩ := hf (Ioo (-ε) ε) (by grind) isOpen_Ioo
  exact ⟨a, ha₁, by grind, ha₃⟩

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : IsFiniteMeasure μ
⊢ μ - μ.singularPart ν = ν.withDensity (μ.rnDeriv ν)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : IsFiniteMeasure μ
⊢ μ - ν.withDensity (μ.rnDeriv ν) = μ.singularPart ν

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
C : ℝ≥0
h : ∀ (x : α), ∃ᶠ (r : ℝ) in 𝓝[>] 0, μ (closedBall x (3 * r)) ≤ ↑C * μ (closedBall x r)
x : α
ε : ℝ
εpos : ε > 0
r : ℝ
μr : μ (closedBall x (3 * r)) ≤ ↑C * μ (closedBall x r)
rpos : 0 < r
rε : r ≤ ε
⊢ closedBall x r ⊆ closedBall x ε

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
C : ℝ≥0
h : ∀ (x : α), ∃ᶠ (r : ℝ) in 𝓝[>] 0, μ (closedBall x (3 * r)) ≤ ↑C * μ (closedBall x r)
x : α
ε : ℝ
εpos : ε > 0
⊢ ∃
    s ∈
      {a |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧ ∃ r, a ⊆ closedBall x r ∧ μ (closedBall x (3 * r)) ≤ ↑C * μ a},
    s ⊆ closedBall x ε

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : s S = 0
hS₃ : ν Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : (μ.singularPart ν) T = 0
hT₃ : ν Tᶜ = 0
hνinter : ν (S ∩ T)ᶜ = 0
A : Set α
hA : MeasurableSet A
⊢ s (A ∩ (S ∩ T)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : s S = 0
hS₃ : ν Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : (μ.singularPart ν) T = 0
hT₃ : ν Tᶜ = 0
hνinter : ν (S ∩ T)ᶜ = 0
A : Set α
hA : MeasurableSet A
hs : s (A ∩ (S ∩ T)) = 0
⊢ (μ.singularPart ν) (A ∩ (S ∩ T)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ ∃ s,
    MeasurableSet s ∧
      (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
h : IsHahnDecomposition μ ν s
⊢ μ.restrict sᶜᶜ ≤ ν.restrict sᶜᶜ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ ∃ s, IsHahnDecomposition μ ν s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : s S = 0
hS₃ : ν Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : (μ.singularPart ν) T = 0
hT₃ : ν Tᶜ = 0
hνinter : ν (S ∩ T)ᶜ = 0
⊢ (ν.withDensity f).restrict (S ∩ T) = (ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a}
hs : s = {x | ∃ᶠ (x : Set α) in v.filterAt x, μ x = 0}
f : α → Set (Set α) := fun x ↦ {a | μ a = 0}
⊢ v.FineSubfamilyOn f s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a}
hs : s = {x | ∃ᶠ (x : Set α) in v.filterAt x, μ x = 0}
f : α → Set (Set α) := fun x ↦ {a | μ a = 0}
h : v.FineSubfamilyOn f s
⊢ ∑' (x : ↑h.index), μ (h.covering ↑x) = ∑' (x : ↑h.index), 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a}
hs : s = {x | ∃ᶠ (x : Set α) in v.filterAt x, μ x = 0}
f : α → Set (Set α) := fun x ↦ {a | μ a = 0}
h : v.FineSubfamilyOn f s
⊢ ∑' (x : ↑h.index), 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝ : SecondCountableTopology α
⊢ ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (fun i ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (fun i ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I : ∀ᶠ (i : ι) in l, ∫ (y : α), g i y • (f y - c) ∂μ + (∫ (y : α), g i y ∂μ) • c = ∫ (y : α), g i y • f y ∂μ
⊢ Tendsto (fun i ↦ ∫ (y : α), g i y • (f y - c) ∂μ) l (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : s S = 0
hS₃ : ν Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : (μ.singularPart ν) T = 0
hT₃ : ν Tᶜ = 0
hνinter : ν (S ∩ T)ᶜ = 0
heq : (ν.withDensity f).restrict (S ∩ T) = (ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T)
A : Set α
hA : MeasurableSet A
⊢ (ν.withDensity f) (A ∩ (S ∩ T)ᶜ) = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : s S = 0
hS₃ : ν Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : (μ.singularPart ν) T = 0
hT₃ : ν Tᶜ = 0
hνinter : ν (S ∩ T)ᶜ = 0
heq : (ν.withDensity f).restrict (S ∩ T) = (ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T)
⊢ ∀ (A : Set α), MeasurableSet A → (ν.withDensity f) A = ((ν.withDensity f).restrict (S ∩ T)) A

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (fun i ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (fun i ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
⊢ Tendsto (fun i ↦ ∫ (y : α), g i y • f y ∂μ) l (𝓝 c)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : s S = 0
hS₃ : ν Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : (μ.singularPart ν) T = 0
hT₃ : ν Tᶜ = 0
hνinter : ν (S ∩ T)ᶜ = 0
heq : (ν.withDensity f).restrict (S ∩ T) = (ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T)
heq' : ∀ (A : Set α), MeasurableSet A → (ν.withDensity f) A = ((ν.withDensity f).restrict (S ∩ T)) A
A : Set α
hA : MeasurableSet A
⊢ (ν.withDensity (μ.rnDeriv ν)) (A ∩ (S ∩ T)ᶜ) = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
ρ ν : Measure α
inst✝ : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a
ε : ℝ≥0
εpos : 0 < ε
x✝ : ν s < ∞
U : Set α
sU : s ⊆ U
U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
νU : ν U ≤ ν s + ↑ε
f : α → Set (Set α) := fun x ↦ {a | ρ a ≤ ν a ∧ a ⊆ U}
⊢ v.FineSubfamilyOn f s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : TopologicalSpace α
f : α → ℝ
hs : IsConnected s
hf : ContinuousOn f s
hint : IntegrableOn f s μ
hμfin : μ s ≠ ∞
hμ0 : μ s ≠ 0
⊢ ∃ c ∈ s, f c = ⨍ (x : α) in s, f x ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
ρ ν : Measure α
inst✝ : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a
ε : ℝ≥0
εpos : 0 < ε
x✝ : ν s < ∞
U : Set α
sU : s ⊆ U
U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
νU : ν U ≤ ν s + ↑ε
f : α → Set (Set α) := fun x ↦ {a | ρ a ≤ ν a ∧ a ⊆ U}
h : v.FineSubfamilyOn f s
this : Encodable ↑h.index
⊢ ∑' (x : ↑h.index), ν (h.covering ↑x) = ν (⋃ x, h.covering ↑x)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
ρ ν : Measure α
inst✝ : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a
⊢ ρ s ≤ ν s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hs : s ⟂ₘ ν
hadd : μ = s + ν.withDensity f
⊢ ν.withDensity f = ν.withDensity (μ.rnDeriv ν)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f ν
hs : s ⟂ₘ ν
hadd : μ = s + ν.withDensity f
⊢ ν.withDensity f = ν.withDensity (μ.rnDeriv ν)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝ : NormedAddCommGroup E
x : α
f : α → E
hf : LocallyIntegrable f μ
⊢ ∀ᶠ (a : Set α) in v.filterAt x, IntegrableOn f a μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst✝ : SigmaFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
⊢ ν.withDensity f = 0 + ν.withDensity f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.DensityTheorem

Goal state before:
pp: α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
Rpos : 0 < R
⊢ ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0, μ (closedBall x (3 * r)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * μ (closedBall x r)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.DensityTheorem

Goal state before:
pp: α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
Rpos : 0 < R
A :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0, μ (closedBall x (3 * r)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * μ (closedBall x r)
⊢ 0 < R / 4

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
s : Set α
hs : MeasurableSet s
⊢ (μ.restrict s).rnDeriv ν =ᵐ[ν] s.indicator (μ.rnDeriv ν)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst✝ : SigmaFinite ν
s : Set α
hs : MeasurableSet s
⊢ (ν.restrict s).rnDeriv ν =ᵐ[ν] s.indicator 1

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.DensityTheorem

Goal state before:
pp: α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
⊢ VitaliFamily μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
this :
  (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
⊢ μ.withDensity ((↑r • ν).rnDeriv μ) = ↑r • μ.withDensity (ν.rnDeriv μ)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ (r • ν).rnDeriv μ =ᵐ[μ] r • ν.rnDeriv μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ ∞
⊢ (r • ν).rnDeriv μ =ᵐ[μ] r • ν.rnDeriv μ

Tactic:
by

Goal state after: