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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
⊢ t = s.singularPart μ

Tactic:
by_cases hfi : Integrable f μ

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : Integrable f μ
⊢ t = s.singularPart μ

case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : ¬Integrable f μ
⊢ t = s.singularPart μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
⊢ ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    (r • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      r • (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

Tactic:
← toSignedMeasure_smul

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
⊢ ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    (r • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (r • s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ p.toReal)
hμs' : ¬μ s = 0
⊢ eLpNorm ((s ∩ {x | ‖f i x‖₊ < C}).indicator (f i)) p μ ≤ ↑C * μ s ^ (1 / p.toReal)

Tactic:
rw [← Set.indicator_indicator]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ p.toReal)
hμs' : ¬μ s = 0
⊢ eLpNorm (s.indicator ({x | ‖f i x‖₊ < C}.indicator (f i))) p μ ≤ ↑C * μ s ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
⊢ ↑(ν s) = ↑ν s

Tactic:
rw [← coeFn_comp_toFiniteMeasure_eq_coeFn, FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure,
    toMeasure_comp_toFiniteMeasure_eq_toMeasure]

Goal state after:
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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
⊢ UnifIntegrable f p μ

Tactic:
refine
    (unifIntegrable_of' hp hp' (fun i => (Exists.choose_spec <| hf i).1) fun ε hε => ?_).ae_eq
      fun i => (Exists.choose_spec <| hf i).2.symm

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
ε : ℝ
hε : 0 < ε
⊢ ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖Exists.choose ⋯ x‖₊}.indicator (Exists.choose ⋯)) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: case right
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key : μ.testAgainstNN f₁ ≤ μ.testAgainstNN f₂ + μ.mass * nndist f₁ f₂
⊢ ↑(μ.testAgainstNN f₁) - ↑(μ.testAgainstNN f₂) ≤ ↑μ.mass * dist f₁ f₂

Tactic:
suffices ↑(μ.testAgainstNN f₁) ≤ ↑(μ.testAgainstNN f₂) + ↑μ.mass * dist f₁ f₂ by linarith

Goal state after:
case right
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key : μ.testAgainstNN f₁ ≤ μ.testAgainstNN f₂ + μ.mass * nndist f₁ f₂
⊢ ↑(μ.testAgainstNN f₁) ≤ ↑(μ.testAgainstNN f₂) + ↑μ.mass * dist f₁ f₂
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case pos.refine_2
α : 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 μ
hp' : 0 < p
hpt : p ≠ ∞
hp : 1 ≤ p.toReal
this : (fun x ↦ ‖μ[f | m] x‖ ^ p.toReal) ≤ᵐ[μ] μ[fun x ↦ ‖f x‖ ^ p.toReal | m]
⊢ ∀ᵐ (a : α) ∂μ, 0 ≤ ‖μ[f | m] a‖ ^ p.toReal

Tactic:
filter_upwards with a

Goal state after:
case pos.refine_2
α : 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 μ
hp' : 0 < p
hpt : p ≠ ∞
hp : 1 ≤ p.toReal
this : (fun x ↦ ‖μ[f | m] x‖ ^ p.toReal) ≤ᵐ[μ] μ[fun x ↦ ‖f x‖ ^ p.toReal | m]
a : α
⊢ 0 ≤ ‖μ[f | m] a‖ ^ p.toReal
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
hμν : μ.toWeakDualBCNN = ν.toWeakDualBCNN
f : Ω →ᵇ ℝ≥0
key : μ.toWeakDualBCNN f = ν.toWeakDualBCNN f
⊢ ∫⁻ (ω : Ω), ↑(f ω) ∂↑μ ≠ ∞

Tactic:
exact (lintegral_lt_top_of_nnreal μ f).ne

Goal state after:
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∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M
ℐ : ℝ≥0 → ι
δ : ℝ≥0
hδpos : 0 < ↑δ
hδ :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal ↑δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hℐ : ∀ (C : ℝ≥0), ENNReal.ofReal ↑δ < μ {x | C ≤ ‖f (ℐ C) x‖₊}
C : ℝ≥0
x : α
hx : x ∈ {x | C ≤ ‖f (ℐ C) x‖₊}
⊢ C ≤ {x | C ≤ ‖f (ℐ C) x‖₊}.indicator (fun a ↦ ‖f (ℐ C) a‖₊) x

Tactic:
Set.indicator_of_mem hx

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M
ℐ : ℝ≥0 → ι
δ : ℝ≥0
hδpos : 0 < ↑δ
hδ :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal ↑δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hℐ : ∀ (C : ℝ≥0), ENNReal.ofReal ↑δ < μ {x | C ≤ ‖f (ℐ C) x‖₊}
C : ℝ≥0
x : α
hx : x ∈ {x | C ≤ ‖f (ℐ C) x‖₊}
⊢ C ≤ ‖f (ℐ C) x‖₊
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
f : Ω → Ω'
f_mble : Measurable f
ν₁ ν₂ : FiniteMeasure Ω
⊢ (ν₁ + ν₂).map f = ν₁.map f + ν₂.map f

Tactic:
by ext; simp [*]

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

Goal state before:
pp: Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω'
inst✝⁵ : TopologicalSpace Ω'
inst✝⁴ : BorelSpace Ω'
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : BorelSpace Ω
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') := {μ | μ (range f)ᶜ = 0}
A : IsEmbedding Subtype.val
μ : FiniteMeasure Ω
⊢ ↑M

Tactic:
refine ⟨μ.map f, ?_⟩

Goal state after:
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω'
inst✝⁵ : TopologicalSpace Ω'
inst✝⁴ : BorelSpace Ω'
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : BorelSpace Ω
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') := {μ | μ (range f)ᶜ = 0}
A : IsEmbedding Subtype.val
μ : FiniteMeasure Ω
⊢ μ.map f ∈ M
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 t2 : Set Ω
ht1 : t1 ∈ s₂
ht2 : t2 ∈ s₁
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
filter_upwards [h t2 t1 ht2 ht1] with a ha

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 Ω
ht1 : t1 ∈ s₂
ht2 : t2 ∈ s₁
a : α
ha : (κ a) (t2 ∩ t1) = (κ a) t2 * (κ a) t1
⊢ (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω'
inst✝⁵ : TopologicalSpace Ω'
inst✝⁴ : BorelSpace Ω'
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : BorelSpace Ω
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') := {μ | μ (range f)ᶜ = 0}
A : IsEmbedding Subtype.val
⊢ ContinuousOn (fun μ ↦ comap f μ) M

Tactic:
exact hf.continuousOn_comap_finiteMeasure

Goal state after:
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : ι → Set Ω
h : iIndepSet f μ
s : Finset ι
⊢ μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)

Tactic:
simpa using Kernel.iIndepSet.meas_biInter h s

Goal state after:
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case mpr
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (Measure.map f μ)
σg : SigmaFinite (Measure.map g μ)
h₀ :
  ∀ {s : Set β} {t : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        μ (f ⁻¹' s) * μ (g ⁻¹' t) = (Measure.map f μ) s * (Measure.map g μ) t ∧
          μ (f ⁻¹' s ∩ g ⁻¹' t) = (Measure.map (fun ω ↦ (f ω, g ω)) μ) (s ×ˢ t)
h : Measure.map (fun ω ↦ (f ω, g ω)) μ = (Measure.map f μ).prod (Measure.map g μ)
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
⊢ μ (f ⁻¹' s ∩ g ⁻¹' t) = (Measure.map f μ) s * (Measure.map g μ) t

Tactic:
(h₀ hs ht).2,

Goal state after:
case mpr
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (Measure.map f μ)
σg : SigmaFinite (Measure.map g μ)
h₀ :
  ∀ {s : Set β} {t : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        μ (f ⁻¹' s) * μ (g ⁻¹' t) = (Measure.map f μ) s * (Measure.map g μ) t ∧
          μ (f ⁻¹' s ∩ g ⁻¹' t) = (Measure.map (fun ω ↦ (f ω, g ω)) μ) (s ×ˢ t)
h : Measure.map (fun ω ↦ (f ω, g ω)) μ = (Measure.map f μ).prod (Measure.map g μ)
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (Measure.map (fun ω ↦ (f ω, g ω)) μ) (s ×ˢ t) = (Measure.map f μ) s * (Measure.map g μ) t
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝ : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
h : Measure.map (fun ω i ↦ f i ω) μ = Measure.pi fun i ↦ Measure.map (f i) μ
S : Finset ι
s : (i : ι) → Set (β i)
hs : ∀ i ∈ S, MeasurableSet (s i)
h₀ :
  ∏ x ∈ S, μ (f x ⁻¹' s x) = (∏ x ∈ S, (Measure.map (f x) μ) (s x)) * ∏ x with x ∉ S, (Measure.map (f x) μ) univ ∧
    μ (⋂ i ∈ S, f i ⁻¹' s i) = (∏ x ∈ S, (Measure.map (f x) μ) (s x)) * ∏ x with x ∉ S, (Measure.map (f x) μ) univ
⊢ μ (⋂ i ∈ S, f i ⁻¹' s i) = ∏ i ∈ S, μ (f i ⁻¹' s i)

Tactic:
h₀.2,

Goal state after:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝ : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
h : Measure.map (fun ω i ↦ f i ω) μ = Measure.pi fun i ↦ Measure.map (f i) μ
S : Finset ι
s : (i : ι) → Set (β i)
hs : ∀ i ∈ S, MeasurableSet (s i)
h₀ :
  ∏ x ∈ S, μ (f x ⁻¹' s x) = (∏ x ∈ S, (Measure.map (f x) μ) (s x)) * ∏ x with x ∉ S, (Measure.map (f x) μ) univ ∧
    μ (⋂ i ∈ S, f i ⁻¹' s i) = (∏ x ∈ S, (Measure.map (f x) μ) (s x)) * ∏ x with x ∉ S, (Measure.map (f x) μ) univ
⊢ (∏ x ∈ S, (Measure.map (f x) μ) (s x)) * ∏ x with x ∉ S, (Measure.map (f x) μ) univ = ∏ i ∈ S, μ (f i ⁻¹' s i)
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
⊢ Indep (generateFrom {t | ∃ n ∈ S, s n = t}) (generateFrom {t | ∃ k ∈ T, s k = t}) η μ

Tactic:
← generateFrom_piiUnionInter_singleton_left,

Goal state after:
case inr
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
⊢ Indep (generateFrom (piiUnionInter (fun k ↦ {s k}) S)) (generateFrom {t | ∃ k ∈ T, s k = t}) η μ
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable X (Measure.map Z μ)
hY : AEStronglyMeasurable Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂Measure.map Z μ) * (Y ω - ∫ (x : Ω), Y x ∂Measure.map Z μ) ∂Measure.map Z μ =
    ∫ (ω : Ω'), (X (Z ω) - ∫ (x : Ω'), X (Z x) ∂μ) * (Y (Z ω) - ∫ (x : Ω'), Y (Z x) ∂μ) ∂μ

Tactic:
rw [integral_map]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable X (Measure.map Z μ)
hY : AEStronglyMeasurable Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ ∫ (x : Ω'), (X (Z x) - ∫ (x : Ω), X x ∂Measure.map Z μ) * (Y (Z x) - ∫ (x : Ω), Y x ∂Measure.map Z μ) ∂μ =
    ∫ (ω : Ω'), (X (Z ω) - ∫ (x : Ω'), X (Z x) ∂μ) * (Y (Z ω) - ∫ (x : Ω'), Y (Z x) ∂μ) ∂μ

case hφ
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable X (Measure.map Z μ)
hY : AEStronglyMeasurable Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ AEMeasurable Z μ

case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable X (Measure.map Z μ)
hY : AEStronglyMeasurable Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ AEStronglyMeasurable (fun ω ↦ (X ω - ∫ (x : Ω), X x ∂Measure.map Z μ) * (Y ω - ∫ (x : Ω), Y x ∂Measure.map Z μ))
    (Measure.map Z μ)
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable X (Measure.map Z μ)
hY : AEStronglyMeasurable Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ ∫ (x : Ω'), (X (Z x) - ∫ (x : Ω), X x ∂Measure.map Z μ) * (Y (Z x) - ∫ (x : Ω), Y x ∂Measure.map Z μ) ∂μ =
    ∫ (ω : Ω'), (X (Z ω) - ∫ (x : Ω'), X (Z x) ∂μ) * (Y (Z ω) - ∫ (x : Ω'), Y (Z x) ∂μ) ∂μ

pp: case hφ
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable X (Measure.map Z μ)
hY : AEStronglyMeasurable Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ AEMeasurable Z μ

pp: case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable X (Measure.map Z μ)
hY : AEStronglyMeasurable Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ AEStronglyMeasurable (fun ω ↦ (X ω - ∫ (x : Ω), X x ∂Measure.map Z μ) * (Y ω - ∫ (x : Ω), Y x ∂Measure.map Z μ))
    (Measure.map Z μ)

Tactic:
rw [integral_map]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable X (Measure.map Z μ)
hY : AEStronglyMeasurable Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ ∫ (x : Ω'), (X (Z x) - ∫ (x : Ω'), X (Z x) ∂μ) * (Y (Z x) - ∫ (x : Ω), Y x ∂Measure.map Z μ) ∂μ =
    ∫ (ω : Ω'), (X (Z ω) - ∫ (x : Ω'), X (Z x) ∂μ) * (Y (Z ω) - ∫ (x : Ω'), Y (Z x) ∂μ) ∂μ

case hφ
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable X (Measure.map Z μ)
hY : AEStronglyMeasurable Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ AEMeasurable Z μ

case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable X (Measure.map Z μ)
hY : AEStronglyMeasurable Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ AEStronglyMeasurable X (Measure.map Z μ)

case hφ
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable X (Measure.map Z μ)
hY : AEStronglyMeasurable Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ AEMeasurable Z μ

case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable X (Measure.map Z μ)
hY : AEStronglyMeasurable Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ AEStronglyMeasurable (fun ω ↦ (X ω - ∫ (x : Ω), X x ∂Measure.map Z μ) * (Y ω - ∫ (x : Ω), Y x ∂Measure.map Z μ))
    (Measure.map Z μ)
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (fun ω ↦ -X ω ^ 2) μ
⊢ ∀ᵐ (a_1 : Ω) ∂μ, ‖X a_1‖ ≤ max |a| |b|

Tactic:
filter_upwards [ha, hb] with ω using abs_le_max_abs_abs

Goal state after:
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: case pos
α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this : {x | ⟨C, ⋯⟩ ≤ ‖f i x‖₊} = {x | C ≤ ‖f i x‖}
⊢ eLpNorm ({x | C ≤ ‖f i x‖}.indicator (f i)) p μ = eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ

Tactic:
← eLpNorm_norm,

Goal state after:
case pos
α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this : {x | ⟨C, ⋯⟩ ≤ ‖f i x‖₊} = {x | C ≤ ‖f i x‖}
⊢ eLpNorm (fun x ↦ ‖{x | C ≤ ‖f i x‖}.indicator (f i) x‖) p μ = eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ
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 : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
h_right : f k = (fun p ↦ p ⟨k, ⋯⟩) ∘ fun a j ↦ f (↑j) a
h_meas_right : Measurable fun p ↦ p ⟨k, ⋯⟩
⊢ IndepFun (fun a ↦ (f i a, f j a)) (f k) κ μ

Tactic:
(Tactic.tacticLet__
 "let"
 (Term.letConfig [])
 (Term.letDecl
  (Term.letIdDecl
   (Term.letId `s)
   []
   [(Term.typeSpec ":" (Term.app `Finset [`ι]))]
   ":="
   (choice
    («term{_}» "{" [`i "," `j] "}")
    (Term.structInst
     "{"
     []
     (Term.structInstFields
      [(Term.structInstField (Term.structInstLVal `i []) []) "," (Term.structInstField (Term.structInstLVal `j []) [])])
     (Term.optEllipsis [])
     []
     "}")))))

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
h_right : f k = (fun p ↦ p ⟨k, ⋯⟩) ∘ fun a j ↦ f (↑j) a
h_meas_right : Measurable fun p ↦ p ⟨k, ⋯⟩
s : Finset ι := {i, j}
⊢ IndepFun (fun a ↦ (f i a, f j a)) (f k) κ μ
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
⊢ filtrationOfSet hsm = natural (fun i ↦ (s i).indicator fun x ↦ 1) ⋯

Tactic:
simp only [filtrationOfSet, natural, measurableSpace_iSup_eq, exists_prop, mk.injEq]

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
⊢ (fun i ↦ MeasurableSpace.generateFrom {t | ∃ j ≤ i, s j = t}) = fun i ↦
    MeasurableSpace.generateFrom {s_1 | ∃ n, MeasurableSet s_1}