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

Goal state before:
pp: α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : ℕ → ℝ := fun i ↦ max 0 (r₁ i)
R₂ : ℕ → ℝ := fun i ↦ max 0 (r₂ i)
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
⊢ blimsup (fun i ↦ cthickening (r₁ i) (s i)) atTop p ≤ᵐ[μ] blimsup (fun i ↦ cthickening (r₂ i) (s i)) atTop p

Tactic:
simp_rw [← cthickening_max_zero (r₁ _), ← cthickening_max_zero (r₂ _)]

Goal state after:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : ℕ → ℝ := fun i ↦ max 0 (r₁ i)
R₂ : ℕ → ℝ := fun i ↦ max 0 (r₂ i)
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
⊢ blimsup (fun i ↦ cthickening (max 0 (r₁ i)) (s i)) atTop p ≤ᵐ[μ]
    blimsup (fun i ↦ cthickening (max 0 (r₂ i)) (s i)) atTop p
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε

Tactic:
by_cases hp_ne_zero : p = 0

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : p = 0
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε

case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝¹ : CompleteSpace E
hm : m ≤ mΩ
inst✝ : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
⊢ μ[fun ω ↦ (B (AEStronglyMeasurable.mk f hf ω)) (g ω) | m] =ᵐ[μ] fun ω ↦
    (B (AEStronglyMeasurable.mk f hf ω)) (μ[g | m] ω)

Tactic:
by
    refine condExp_stronglyMeasurable_bilin_of_bound B hm hf.stronglyMeasurable_mk
      hg c ?_
    filter_upwards [hf_bound, hf.ae_eq_mk] with ω hω1 hω2
    rwa [← hω2]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < n), s.restrictNonposSeq i k] 0
⊢ 0 < s (s.restrictNonposSeq i n)

Tactic:
by
  cases n with
  | zero =>
    rw [restrictNonposSeq]; rw [← @Set.sdiff_empty _ i] at hi₂
    rcases someExistsOneDivLT_spec hi₂ with ⟨_, _, h⟩
    exact lt_trans Nat.one_div_pos_of_nat h
  | succ n =>
    rw [restrictNonposSeq_succ]
    have h₁ : ¬s ≤[i \ ⋃ (k : ℕ) (_ : k ≤ n), restrictNonposSeq s i k] 0 := by
      refine mt (restrict_le_zero_subset _ ?_ (by simp)) hn
      convert! measurable_of_not_restrict_le_zero _ hn using 3
      exact funext fun x => by rw [Nat.lt_succ_iff]
    rcases someExistsOneDivLT_spec h₁ with ⟨_, _, h⟩
    exact lt_trans Nat.one_div_pos_of_nat h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ?m.82 s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p ?m.82 ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal ε

Tactic:
rw [(_ : f = { x : α | M ≤ ‖f x‖₊ }.indicator f + { x : α | ‖f x‖ < M }.indicator f)]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ?m.82 s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p ?m.82 ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator ({x | M ≤ ↑‖f x‖₊}.indicator f + {x | ‖f x‖ < M}.indicator f)) p μ ≤ 2 * ENNReal.ofReal ε

α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ?m.82 s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p ?m.82 ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ f = {x | M ≤ ↑‖f x‖₊}.indicator f + {x | ‖f x‖ < M}.indicator f
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : v ≤[i] w
hj₁ : MeasurableSet j
hj₂ : v ≤[j] w
⊢ v ≤[i ∪ j] w

Tactic:
Set.union_eq_iUnion

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : v ≤[i] w
hj₁ : MeasurableSet j
hj₂ : v ≤[j] w
⊢ v ≤[⋃ b, bif b then i else j] w
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : MeasurableSet i
⊢ s i = s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i

Tactic:
grind [Measure.toSignedMeasure_sub_apply, toSignedMeasure, toSignedMeasure_toJordanDecomposition]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : MeasurableSet i
⊢ s i = s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i

Tactic:
by
  grind [Measure.toSignedMeasure_sub_apply, toSignedMeasure, toSignedMeasure_toJordanDecomposition]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
g : α → E
hf : AEMeasurable f μ
hfg : Integrable (f • g) μ
⊢ μ.withDensityᵥ (f • g) = (μ.withDensity fun x ↦ ↑(f x)).withDensityᵥ g

Tactic:
ext s hs
  rw [withDensityᵥ_apply hfg hs,
    withDensityᵥ_apply ((integrable_withDensity_iff_integrable_smul₀ hf).mpr hfg) hs,
    setIntegral_withDensity_eq_setIntegral_smul₀ hf.restrict _ hs]
  simp only [Pi.smul_apply']

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : s ≤[i] 0
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ (s.toMeasureOfLEZero i hi₁ hi).real j = -s (i ∩ j)

Tactic:
by
  simp [measureReal_def, toMeasureOfLEZero_apply _ hi hi₁ hj₁]

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd :
  s =
    t +
      if hf : Integrable f μ then
        { measureOf' := fun s ↦ if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0, empty' := ⋯,
          not_measurable' := ⋯, m_iUnion' := ⋯ }
      else 0
hfi : ¬Integrable f μ
⊢ s.HaveLebesgueDecomposition μ

Tactic:
dif_neg hfi,

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + 0
hfi : ¬Integrable f μ
⊢ s.HaveLebesgueDecomposition μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd :
  s =
    t +
      if hf : Integrable f μ then
        { measureOf' := fun s ↦ if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0, empty' := ⋯,
          not_measurable' := ⋯, m_iUnion' := ⋯ }
      else 0
hfi : ¬Integrable f μ
⊢ t = s.singularPart μ

Tactic:
dif_neg hfi,

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + 0
hfi : ¬Integrable f μ
⊢ t = s.singularPart μ
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

Goal state before:
pp: Ω : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun n ω ↦ ↑((thickenedIndicator ⋯ F) ω)
h_eq : ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑((thickenedIndicator ⋯ F) ω) ∂μ = ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)
h : Tendsto (fun n ↦ ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)) atTop (𝓝 (μ F))
⊢ Tendsto (fun n ↦ ∫ (ω : Ω), ↑((thickenedIndicator ⋯ F) ω) ∂μ) atTop (𝓝 (μ.real F))

Tactic:
Measure.real_def

Goal state after:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun n ω ↦ ↑((thickenedIndicator ⋯ F) ω)
h_eq : ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑((thickenedIndicator ⋯ F) ω) ∂μ = ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)
h : Tendsto (fun n ↦ ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)) atTop (𝓝 (μ F))
⊢ Tendsto (fun n ↦ ∫ (ω : Ω), ↑((thickenedIndicator ⋯ F) ω) ∂μ) atTop (𝓝 (μ F).toReal)
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x✝ : ↑{g | ∃ ni, ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (ni n) x) u (𝓝 (g x))}
t : Set α
ht : MeasurableSet t
ht' : μ t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (s n) x) u (𝓝 (f x))
a : α
ha : Tendsto (fun n ↦ fn (s n) a) u (𝓝 (f a))
⊢ Tendsto (fun x ↦ t.indicator (fn (s x)) a) u (𝓝 (t.indicator f a))

Tactic:
by_cases memt : a ∈ t

Goal state after:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x✝ : ↑{g | ∃ ni, ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (ni n) x) u (𝓝 (g x))}
t : Set α
ht : MeasurableSet t
ht' : μ t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (s n) x) u (𝓝 (f x))
a : α
ha : Tendsto (fun n ↦ fn (s n) a) u (𝓝 (f a))
memt : a ∈ t
⊢ Tendsto (fun x ↦ t.indicator (fn (s x)) a) u (𝓝 (t.indicator f a))

case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x✝ : ↑{g | ∃ ni, ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (ni n) x) u (𝓝 (g x))}
t : Set α
ht : MeasurableSet t
ht' : μ t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (s n) x) u (𝓝 (f x))
a : α
ha : Tendsto (fun n ↦ fn (s n) a) u (𝓝 (f a))
memt : a ∉ t
⊢ Tendsto (fun x ↦ t.indicator (fn (s x)) a) u (𝓝 (t.indicator f a))
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
p : ℝ≥0∞
hp : 1 ≤ p
hf : MemLp f p μ
h✝ : NeZero μ
hp' : 0 < p
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
hpt : p ≠ ∞
⊢ lpNorm μ[f | m] p μ ≤ (∫ (x : α), ‖f x‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹

Tactic:
lpNorm_eq_integral_norm_rpow_toReal hp'.ne.symm hpt integrable_condExp.1

Goal state after:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
p : ℝ≥0∞
hp : 1 ≤ p
hf : MemLp f p μ
h✝ : NeZero μ
hp' : 0 < p
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
hpt : p ≠ ∞
⊢ (∫ (x : α), ‖μ[f | m] x‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹ ≤ (∫ (x : α), ‖f x‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

Tactic:
rw [FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto]; rfl

Goal state after:
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
⊢ ContinuousSMul ℝ≥0 (FiniteMeasure Ω)

Tactic:
refine ⟨continuous_iff_continuousAt.2 (fun p ↦ ?_)⟩
  apply tendsto_iff_forall_integral_tendsto.2 (fun g ↦ ?_)
  have A : Tendsto (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ i.1) (𝓝 p) (𝓝 (p.1)) := by
    rw [nhds_prod_eq]
    exact tendsto_fst
  have B : Tendsto (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ ∫ x, g x ∂i.2) (𝓝 p)
      (𝓝 (∫ x, g x ∂p.2)) := by
    rw [nhds_prod_eq]
    exact (tendsto_iff_forall_integral_tendsto.1 tendsto_id g).comp tendsto_snd
  convert! A.smul B with q <;> simp

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s₁ s₂ : Set (Set Ω)
h : IndepSets s₁ s₂ κ μ
t1 : Set Ω
⊢ ∀ (t2 : Set Ω), t1 ∈ s₂ → t2 ∈ s₁ → ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
t2

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s₁ s₂ : Set (Set Ω)
h : IndepSets s₁ s₂ κ μ
t1 t2 : Set Ω
⊢ t1 ∈ s₂ → t2 ∈ s₁ → ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s₁ s₂ s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h₁ : IndepSets s₁ s' κ μ
h₂ : IndepSets s₂ s' κ μ
t1 : Set Ω
⊢ ∀ (t2 : Set Ω), t1 ∈ s₁ ∪ s₂ → t2 ∈ s' → ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
t2

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s₁ s₂ s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h₁ : IndepSets s₁ s' κ μ
h₂ : IndepSets s₂ s' κ μ
t1 t2 : Set Ω
⊢ t1 ∈ s₁ ∪ s₂ → t2 ∈ s' → ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
hyp : ∀ (n : ι), IndepSets (s n) s' κ μ
t1 : Set Ω
⊢ ∀ (t2 : Set Ω), t1 ∈ ⋃ n, s n → t2 ∈ s' → ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
t2

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
hyp : ∀ (n : ι), IndepSets (s n) s' κ μ
t1 t2 : Set Ω
⊢ t1 ∈ ⋃ n, s n → t2 ∈ s' → ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
hyp : ∀ n ∈ u, IndepSets (s n) s' κ μ
t1 : Set Ω
⊢ ∀ (t2 : Set Ω), t1 ∈ ⋃ n ∈ u, s n → t2 ∈ s' → ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
t2

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
hyp : ∀ n ∈ u, IndepSets (s n) s' κ μ
t1 t2 : Set Ω
⊢ t1 ∈ ⋃ n ∈ u, s n → t2 ∈ s' → ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h : ∃ n, IndepSets (s n) s' κ μ
t1 : Set Ω
⊢ ∀ (t2 : Set Ω), t1 ∈ ⋂ n, s n → t2 ∈ s' → ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
t2

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h : ∃ n, IndepSets (s n) s' κ μ
t1 t2 : Set Ω
⊢ t1 ∈ ⋂ n, s n → t2 ∈ s' → ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
h : ∃ n ∈ u, IndepSets (s n) s' κ μ
t1 : Set Ω
⊢ ∀ (t2 : Set Ω), t1 ∈ ⋂ n ∈ u, s n → t2 ∈ s' → ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
t2

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
h : ∃ n ∈ u, IndepSets (s n) s' κ μ
t1 t2 : Set Ω
⊢ t1 ∈ ⋂ n ∈ u, s n → t2 ∈ s' → ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
f : Ω → ℝ
f_cont : Continuous[inst✝¹, _] f
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen[inst✝¹] G → μ G ≤ liminf (fun i ↦ (μs i) G) atTop
⊢ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i ↦ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop

Tactic:
simp_rw [lintegral_eq_lintegral_meas_lt _ (Eventually.of_forall f_nn) f_cont.aemeasurable]

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
f : Ω → ℝ
f_cont : Continuous[inst✝¹, _] f
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen[inst✝¹] G → μ G ≤ liminf (fun i ↦ (μs i) G) atTop
⊢ ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} ≤ liminf (fun i ↦ ∫⁻ (t : ℝ) in Ioi 0, (μs i) {a | t < f a}) atTop
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h : IsMarkovKernel κ
t1 : Set Ω
⊢ ∀ (t2 : Set Ω),
    t1 ∈ {s | MeasurableSet s} → t2 ∈ {s | MeasurableSet s} → ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
t2

Goal state after:
case inr
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h : IsMarkovKernel κ
t1 t2 : Set Ω
⊢ t1 ∈ {s | MeasurableSet s} → t2 ∈ {s | MeasurableSet s} → ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬pdf X ℙ μ =ᵐ[μ] 0
⊢ HasPDF X ℙ μ

Tactic:
by
  refine ⟨?_, ?_, hac⟩
  · exact aemeasurable_of_pdf_ne_zero X hpdf
  · contrapose hpdf
    have := pdf_of_not_haveLebesgueDecomposition hpdf
    filter_upwards using congrFun this

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr.refine_3
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
⊢ IndepSets (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S) (piiUnionInter (fun n ↦ {s | MeasurableSet s}) T) η μ

Tactic:
· exact indepSets_piiUnionInter_of_disjoint (h_indep.congr η_eq) hST

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
X Y : Ω → G
inst✝² : SFinite μ
inst✝¹ : HasPDF X ℙ μ
inst✝ : HasPDF Y ℙ μ
σX : SigmaFinite (map X ℙ)
σY : SigmaFinite (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this✝ : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
⊢ (map X ℙ ∗ₘ map Y ℙ).HaveLebesgueDecomposition μ

Tactic:
apply HaveLebesgueDecomposition.mconv

Goal state after:
case hν₁
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
X Y : Ω → G
inst✝² : SFinite μ
inst✝¹ : HasPDF X ℙ μ
inst✝ : HasPDF Y ℙ μ
σX : SigmaFinite (map X ℙ)
σY : SigmaFinite (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this✝ : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
⊢ map X ℙ ≪ μ

case hν₂
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
X Y : Ω → G
inst✝² : SFinite μ
inst✝¹ : HasPDF X ℙ μ
inst✝ : HasPDF Y ℙ μ
σX : SigmaFinite (map X ℙ)
σY : SigmaFinite (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this✝ : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
⊢ map Y ℙ ≪ μ