mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ l, s.restrictNonposSeq i l
hA : A = i \ ⋃ l, s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun n ↦ s.findExistsOneDivLT (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : s i = s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
h₂ : s A ≤ s i
h₃' : Summable fun n ↦ 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n ↦ ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n ↦ ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : 0 E < s E
⊢ False

Tactic:
have : ∃ k, 1 ≤ bdd k ∧ 1 / (bdd k : ℝ) < s E := by
    rw [tendsto_atTop_atTop] at h₄
    obtain ⟨k, hk⟩ := h₄ (max (1 / s E + 1) 1)
    refine ⟨k, ?_, ?_⟩
    · have hle := le_of_max_le_right (hk k le_rfl)
      norm_cast at hle
    · have : 1 / s E < bdd k := by
        linarith only [le_of_max_le_left (hk k le_rfl)]
      rw [one_div] at this ⊢
      exact inv_lt_of_inv_lt₀ hE₃ this

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ l, s.restrictNonposSeq i l
hA : A = i \ ⋃ l, s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun n ↦ s.findExistsOneDivLT (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : s i = s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
h₂ : s A ≤ s i
h₃' : Summable fun n ↦ 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n ↦ ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n ↦ ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : 0 E < s E
this : ∃ k, 1 ≤ bdd k ∧ 1 / ↑(bdd k) < s E
⊢ False
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ (s.toJordanDecomposition.posPart.singularPart μ +
          μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)).toSignedMeasure -
      (μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ) +
          s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure

Tactic:
convert! rfl

Goal state after:
case e'_3.e'_5
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.posPart =
    s.toJordanDecomposition.posPart.singularPart μ + μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)

case e'_3.e'_6
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.negPart =
    μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ) + s.toJordanDecomposition.negPart.singularPart μ
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = (fun x ↦ g) + fun n ↦ f n - g
⊢ UnifIntegrable (fun x ↦ g) p μ

pp: case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = (fun x ↦ g) + fun n ↦ f n - g
⊢ UnifIntegrable (fun n ↦ f n - g) p μ

Tactic:
· exact unifIntegrable_const hp hp' hg

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = (fun x ↦ g) + fun n ↦ f n - g
⊢ UnifIntegrable (fun n ↦ f n - g) p μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ (c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ)) i = ((re c).toComplexMeasure (im c)) i

Tactic:
add_apply,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ (c.singularPart μ) i + (μ.withDensityᵥ (c.rnDeriv μ)) i = ((re c).toComplexMeasure (im c)) i
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
⊢ ∫ (x : α), |μ[f | m] x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

Tactic:
by
  by_cases! hm : ¬ m ≤ m0
  · simpa [condExp_of_not_le hm] using integral_nonneg (fun x => abs_nonneg f x)
  by_cases! hsig : ¬ SigmaFinite (μ.trim hm)
  · simpa [condExp_of_not_sigmaFinite hm hsig] using integral_nonneg (fun x => abs_nonneg f x)
  calc
  _ ≤ ∫ x, μ[|f| | m] x ∂μ :=
    integral_mono_ae integrable_condExp.abs integrable_condExp (abs_condExp_ae_le_condExp_abs f)
  _ = _ := integral_condExp hm

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case pos.refine_2.refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f μ
h : 0 < μ {x | ↑R < |μ[f | m] x|}
⊢ MeasurableSet {x | ↑R < |μ[f | m] x|}

Tactic:
simp_rw [← Real.norm_eq_abs]
    exact @measurableSet_lt _ _ _ _ _ m _ _ _ _ _ measurable_const
      stronglyMeasurable_condExp.norm.measurable

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
hμ : μ = 0
⊢ μ.mass = 0

Tactic:
by simp only [hμ, zero_mass]

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (ω : Ω), ↑(f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂↑μ))

Tactic:
rw [tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds]
  exact FiniteMeasure.tendsto_iff_forall_lintegral_tendsto

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

Goal state before:
pp: Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ ↑μ.normalize = μ.mass⁻¹ • ↑μ

Tactic:
ext1 s _s_mble

Goal state after:
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
s : Set Ω
_s_mble : MeasurableSet s
⊢ ↑μ.normalize s = (μ.mass⁻¹ • ↑μ) s
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
⊢ testAgainstNN 0 = 0

Tactic:
by
  funext
  simp only [zero_testAgainstNN_apply, Pi.zero_apply]

Goal state after:
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 (fun i ↦ (μs i).toWeakDualBCNN) F (𝓝 μ.toWeakDualBCNN) ↔
    ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ (μs i).toWeakDualBCNN f) F (𝓝 (μ.toWeakDualBCNN f))

Tactic:
tendsto_iff_forall_eval_tendsto_topDualPairing

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ (∀ (y : Ω →ᵇ ℝ≥0),
      Tendsto (fun i ↦ ((topDualPairing ℝ≥0 (Ω →ᵇ ℝ≥0)) (μs i).toWeakDualBCNN) y) F
        (𝓝 (((topDualPairing ℝ≥0 (Ω →ᵇ ℝ≥0)) μ.toWeakDualBCNN) y))) ↔
    ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ (μs i).toWeakDualBCNN f) F (𝓝 (μ.toWeakDualBCNN f))
Module: Mathlib.MeasureTheory.Measure.Tight

Goal state before:
pp: case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst✝⁴ : TopologicalSpace 𝓧
inst✝³ : TopologicalSpace 𝓨
inst✝² : MeasurableSpace 𝓨
inst✝¹ : OpensMeasurableSpace 𝓨
inst✝ : T2Space 𝓨
hS : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
f : 𝓧 → 𝓨
hf : Continuous[inst✝⁴, inst✝³] f
ε : ENNReal
hε : 0 < ε
K : Set 𝓧
hK_compact : IsCompact K
hKS : ∀ μ ∈ S, μ Kᶜ ≤ ε
μ : Measure 𝓧
hμS : μ ∈ S
hf_meas : AEMeasurable f μ
⊢ (Measure.map f μ) (f '' K)ᶜ ≤ ε

Tactic:
Measure.map_apply_of_aemeasurable hf_meas (hK_compact.image hf).measurableSet.compl

Goal state after:
case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst✝⁴ : TopologicalSpace 𝓧
inst✝³ : TopologicalSpace 𝓨
inst✝² : MeasurableSpace 𝓨
inst✝¹ : OpensMeasurableSpace 𝓨
inst✝ : T2Space 𝓨
hS : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
f : 𝓧 → 𝓨
hf : Continuous[inst✝⁴, inst✝³] f
ε : ENNReal
hε : 0 < ε
K : Set 𝓧
hK_compact : IsCompact K
hKS : ∀ μ ∈ S, μ Kᶜ ≤ ε
μ : Measure 𝓧
hμS : μ ∈ S
hf_meas : AEMeasurable f μ
⊢ μ (f ⁻¹' (f '' K)ᶜ) ≤ ε
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen[inst✝²] G → μ G ≤ liminf (fun i ↦ (μs i) G) atTop
same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i ↦ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
g : Ω →ᵇ ℝ≥0 := comp Real.toNNReal Real.lipschitzWith_toNNReal f
bound : ∀ (i : ℕ), ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i ≤ ↑(nndist 0 g)
⊢ liminf (fun i ↦ (∫⁻ (a : Ω), ENNReal.ofReal (f a) ∂μs i).toReal) atTop =
    (liminf (fun i ↦ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop).toReal

Tactic:
apply ENNReal.liminf_toReal_eq ENNReal.coe_ne_top (Eventually.of_forall bound)

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝⁴ : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst✝³ : IsFiniteMeasure ℙ
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : HasPDF (fun ω ↦ (X ω, Y ω)) ℙ (μ.prod ν)
⊢ X ⟂ᵢ[ℙ] Y ↔ pdf (fun ω ↦ (X ω, Y ω)) ℙ (μ.prod ν) =ᵐ[μ.prod ν] fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2

Tactic:
by
  have : HasPDF X ℙ μ := quasiMeasurePreserving_hasPDF' (μ := μ.prod ν) (fun ω ↦ (X ω, Y ω))
    quasiMeasurePreserving_fst
  have : HasPDF Y ℙ ν := quasiMeasurePreserving_hasPDF' (μ := μ.prod ν) (fun ω ↦ (X ω, Y ω))
    quasiMeasurePreserving_snd
  have h₀ : (ℙ.map X).prod (ℙ.map Y) =
      (μ.prod ν).withDensity fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2 :=
    prod_eq fun s t hs ht ↦ by rw [withDensity_apply _ (hs.prod ht), ← prod_restrict,
      lintegral_prod_mul (measurable_pdf X ℙ μ).aemeasurable (measurable_pdf Y ℙ ν).aemeasurable,
      map_eq_setLIntegral_pdf X ℙ μ hs, map_eq_setLIntegral_pdf Y ℙ ν ht]
  rw [indepFun_iff_map_prod_eq_prod_map_map (HasPDF.aemeasurable X ℙ μ) (HasPDF.aemeasurable Y ℙ ν),
    ← eq_of_map_eq_withDensity, h₀]
  exact (((measurable_pdf X ℙ μ).comp measurable_fst).mul
    ((measurable_pdf Y ℙ ν).comp measurable_snd)).aemeasurable

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst✝¹] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst✝¹] G
r : ℝ≥0
hr : r < ν G
s : ↑G → Set Ω
hsS : ∀ (x : ↑G), s x ∈ S
hs_nhds : ∀ (x : ↑G), s x ∈ 𝓝 ↑x
hsG : ∀ (x : ↑G), s x ⊆ G
T₀ : Set ↑G
T₀_count : T₀.Countable
hT₀ : ⋃ i ∈ T₀, interior (s i) = ⋃ i, interior (s i)
⊢ G ⊆ ⋃ i, interior (s i)

Tactic:
intro y

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst✝¹] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst✝¹] G
r : ℝ≥0
hr : r < ν G
s : ↑G → Set Ω
hsS : ∀ (x : ↑G), s x ∈ S
hs_nhds : ∀ (x : ↑G), s x ∈ 𝓝 ↑x
hsG : ∀ (x : ↑G), s x ⊆ G
T₀ : Set ↑G
T₀_count : T₀.Countable
hT₀ : ⋃ i ∈ T₀, interior (s i) = ⋃ i, interior (s i)
y : Ω
⊢ y ∈ G → y ∈ ⋃ i, interior (s i)
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case iSup.h_mono
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
⊢ Monotone fun i ω ↦ f ω * f' i ω

Tactic:
· exact fun n m (h_le : n ≤ m) a => mul_le_mul_right (h_mono_f' h_le a) _

Goal state after:
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: case insert
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
inst✝ : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : (∀ i ∈ s, MemLp (X i) 2 μ) → cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ cov[∑ i ∈ insert i s, X i, Y; μ] = ∑ i ∈ insert i s, cov[X i, Y; μ]

Tactic:
| insert i s hi h_ind =>

Goal state after:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case neg.hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
⊢ 0 ≤ᵐ[μ] fun ω ↦ (X ω - ∫ (x : Ω), X x ∂μ) ^ 2

Tactic:
exact Eventually.of_forall fun x => sq_nonneg _

Goal state after:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
⊢ Var[X + Y; μ] = Var[X; μ] + Var[Y; μ]

Tactic:
by_cases h' : X =ᵐ[μ] 0
  · rw [variance_congr h', variance_congr h'.add_right]
    simp
  have := hX.isProbabilityMeasure_of_indepFun X Y (by simp) (by simp) h' h
  rw [variance_add hX hY, h.covariance_eq_zero hX hY]
  simp

Goal state after:
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝³ : ConditionallyCompleteLinearOrder γ
inst✝² : TopologicalSpace γ
inst✝¹ : OpensMeasurableSpace γ
inst✝ : OrderClosedTopology γ
h : IdentDistrib f g μ ν
I : ∀ (a : γ), μ {x | a < f x} = ν {x | a < g x}
⊢ essSup f μ = essSup g ν

Tactic:
essSup_eq_sInf,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝³ : ConditionallyCompleteLinearOrder γ
inst✝² : TopologicalSpace γ
inst✝¹ : OpensMeasurableSpace γ
inst✝ : OrderClosedTopology γ
h : IdentDistrib f g μ ν
I : ∀ (a : γ), μ {x | a < f x} = ν {x | a < g x}
⊢ sInf {a | μ {x | a < f x} = 0} = sInf {a | ν {x | a < g x} = 0}
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : Mul β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
this : IndepFun (fun ω ↦ (f i ω, f j ω)) (f k) κ μ
⊢ IndepFun (f i * f j) (f k) κ μ

Tactic:
simpa using! this.comp (measurable_fst.mul measurable_snd) measurable_id

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : Mul β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
this : IndepFun (fun ω ↦ (f i ω, f j ω)) (f k) κ μ
⊢ IndepFun (f i * f j) (f k) κ μ

Tactic:
simpa using! this.comp (measurable_fst.mul measurable_snd) measurable_id

Goal state after:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
x✝ : Set (Filtration ι m)
hn : ¬x✝.Nonempty
⊢ IsGLB x✝ { seq := fun i ↦ m, mono' := ⋯, le' := ⋯ }

Tactic:
· rw [Set.not_nonempty_iff_eq_empty] at hn
      simpa [hn] using! Filtration.le

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

Goal state before:
pp: case refine_3.refine_1.refine_2
α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n)
f : ℕ → α → ℝ≥0∞ := fun n ↦ (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), (s k).indicator 1
hfapp : ∀ (n : ℕ) (a : α), f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun x_1 ↦ f x_1 x) atTop ∂μ ≤ μ univ
x : α
hxN : x ∉ N
hx : r / μ univ ≤ limsup (fun x_1 ↦ f x_1 x) atTop
hxs : {n | x ∈ s n}.Finite
n : ℕ
⊢ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1) x ≤ ↑hxs.toFinset.card

Tactic:
simpa only [Finset.sum_apply, indicator_apply, Pi.one_apply, Finset.sum_boole, Nat.cast_le]
          using! Finset.card_le_card fun m hm ↦ hxs.mem_toFinset.2 (Finset.mem_filter.1 hm).2

Goal state after:
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
⊢ ∃ x, x ≠ 0 ∧ ↑x ∈ s

Tactic:
have h_mes : μ s ≠ 0 := fun hμ ↦ fund.measure_ne_zero (NeZero.ne μ) <| by simpa [hμ] using h

Goal state after:
E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
⊢ ∃ x, x ≠ 0 ∧ ↑x ∈ s
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
f g : α →C_c ℝ
⊢ (f + g).nnrealPart ≤ f.nnrealPart + g.nnrealPart

Tactic:
by
  intro x
  simpa using Real.toNNReal_add_le

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
⊢ ‖∫ᶜ (x : E) in Path.segment a b, ω x - (ω a) (b - a)‖ ≤ ε * ‖b - a‖

Tactic:
have hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s :=
    ((convex_ball _ _).inter hs).segment_subset (by simp [*]) (by simp [*])

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
⊢ ‖∫ᶜ (x : E) in Path.segment a b, ω x - (ω a) (b - a)‖ ≤ ε * ‖b - a‖
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
a : E
ω : E → E →L[𝕜] F
hω : ∀ᶠ (z : E) in 𝓝 a, ContinuousAt ω z
⊢ ∀ᶠ (x : E) in 𝓝[univ] a, ContinuousWithinAt ω univ x

Tactic:
simpa only [nhdsWithin_univ, continuousWithinAt_univ]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, ‖fderiv ℝ f x‖ ≤ C
hmem_s : ∀ t ∈ Ioo 0 1, (lineMap a b) t ∈ s
hC₀ : 0 ≤ C
hfc : ContinuousOn f (segment ℝ a b)
hfd : ∀ t ∈ Ioo 0 1, LineDifferentiableAt ℝ f ((lineMap a b) t) (b - a)
t : ℝ
ht : t ∈ Ioo 0 1
⊢ DifferentiableAt ℝ f ((lineMap a b) t)

Tactic:
· exact hf.differentiableAt hs <| hmem_s t ht

Goal state after:
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K1 K2 : Compacts X
⊢ rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2

Tactic:
apply _root_.le_of_forall_pos_le_add

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K1 K2 : Compacts X
⊢ ∀ (ε : ℝ≥0), 0 < ε → rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case pos
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), 0 ≤ f x ∧ f x ≤ 1
V : Set X
hV : tsupport ⇑f ⊆ V
this :
  (rieszContent (toNNRealLinear Λ)).measure ↑{ carrier := tsupport ⇑f, isCompact' := ⋯ } =
    (rieszContent (toNNRealLinear Λ)) { carrier := tsupport ⇑f, isCompact' := ⋯ }
ε✝ : NNReal
hε : 0 < ε✝
g : X →C_c NNReal
hg :
  (∀ x ∈ { carrier := tsupport ⇑f, isCompact' := ⋯ }, 1 ≤ g x) ∧
    (toNNRealLinear Λ) g < rieszContentAux (toNNRealLinear Λ) { carrier := tsupport ⇑f, isCompact' := ⋯ } + ε✝
x : X
hx : x ∈ tsupport ⇑f
⊢ f x ≤ (toRealLinearMap g) x

Tactic:
simpa using le_trans (hf x).2 (hg.1 x hx)

Goal state after: