mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
f g : Dual K V
v : V
a b : K
hv : ∀ (s t : K), s • (↑e).fixedSubmodule.mkQ v + t • e.fixedReduce ((↑e).fixedSubmodule.mkQ v) = 0 → s = 0 ∧ t = 0
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
hg0 : g ≠ 0
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
ha : ∀ (v_1 : V), (auxTransvection hf * e) v_1 - a • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hb : ∀ (v_1 : V), (auxTransvection hg * e) v_1 - b • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
c : K := b - a
hc : c = b - a
key : ∀ (x : V), g (e x) • (v - e v) - c • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hc0 : c = 0
y : V
hy : -y ∈ (↑e).fixedSubmodule
k : K
hk : v - e v - k • v = y
⊢ (k - 1) • v + 1 • e v = -y

Tactic:
rw [← hk]

Goal state after:
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
f g : Dual K V
v : V
a b : K
hv : ∀ (s t : K), s • (↑e).fixedSubmodule.mkQ v + t • e.fixedReduce ((↑e).fixedSubmodule.mkQ v) = 0 → s = 0 ∧ t = 0
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
hg0 : g ≠ 0
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
ha : ∀ (v_1 : V), (auxTransvection hf * e) v_1 - a • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hb : ∀ (v_1 : V), (auxTransvection hg * e) v_1 - b • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
c : K := b - a
hc : c = b - a
key : ∀ (x : V), g (e x) • (v - e v) - c • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hc0 : c = 0
y : V
hy : -y ∈ (↑e).fixedSubmodule
k : K
hk : v - e v - k • v = y
⊢ (k - 1) • v + 1 • e v = -(v - e v - k • v)
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case succ.inr
α : Type u_1
C : Set (Set α)
s t : Set α
I✝ : Finset (Set α)
G✝ : Type u_2
inst✝² : AddCommMonoid G✝
m m' : AddContent G✝ C
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)),
    ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} →
      (↑I).PairwiseDisjoint id →
        ⋃₀ ↑I ∈ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} → #I = n → onIocAux f (⋃₀ ↑I) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv✝ : u ≤ v
h'uv : ⋃₀ ↑I = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ ↑I
u' : α
uu' : u ≤ u'
hu'v' : u' ≤ v
tI : Set.Ioc u' v ∈ I
ht : v ∈ Set.Ioc u' v
left✝ : v ≤ v
I' : Finset (Set α) := I.erase (Set.Ioc u' v)
I'I : I' ⊆ I
I_eq_insert : I = insert (Set.Ioc u' v) I'
UI' : ⋃₀ ↑I' = Set.Ioc u u'
IH : onIocAux f (⋃₀ ↑I') = ∑ u ∈ I', onIocAux f u
⊢ f v - f u = ∑ u ∈ insert (Set.Ioc u' v) I', onIocAux f u

Tactic:
sum_insert,

Goal state after:
case succ.inr
α : Type u_1
C : Set (Set α)
s t : Set α
I✝ : Finset (Set α)
G✝ : Type u_2
inst✝² : AddCommMonoid G✝
m m' : AddContent G✝ C
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)),
    ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} →
      (↑I).PairwiseDisjoint id →
        ⋃₀ ↑I ∈ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} → #I = n → onIocAux f (⋃₀ ↑I) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv✝ : u ≤ v
h'uv : ⋃₀ ↑I = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ ↑I
u' : α
uu' : u ≤ u'
hu'v' : u' ≤ v
tI : Set.Ioc u' v ∈ I
ht : v ∈ Set.Ioc u' v
left✝ : v ≤ v
I' : Finset (Set α) := I.erase (Set.Ioc u' v)
I'I : I' ⊆ I
I_eq_insert : I = insert (Set.Ioc u' v) I'
UI' : ⋃₀ ↑I' = Set.Ioc u u'
IH : onIocAux f (⋃₀ ↑I') = ∑ u ∈ I', onIocAux f u
⊢ f v - f u = onIocAux f (Set.Ioc u' v) + ∑ x ∈ I', onIocAux f x

case succ.inr
α : Type u_1
C : Set (Set α)
s t : Set α
I✝ : Finset (Set α)
G✝ : Type u_2
inst✝² : AddCommMonoid G✝
m m' : AddContent G✝ C
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)),
    ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} →
      (↑I).PairwiseDisjoint id →
        ⋃₀ ↑I ∈ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} → #I = n → onIocAux f (⋃₀ ↑I) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv✝ : u ≤ v
h'uv : ⋃₀ ↑I = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ ↑I
u' : α
uu' : u ≤ u'
hu'v' : u' ≤ v
tI : Set.Ioc u' v ∈ I
ht : v ∈ Set.Ioc u' v
left✝ : v ≤ v
I' : Finset (Set α) := I.erase (Set.Ioc u' v)
I'I : I' ⊆ I
I_eq_insert : I = insert (Set.Ioc u' v) I'
UI' : ⋃₀ ↑I' = Set.Ioc u u'
IH : onIocAux f (⋃₀ ↑I') = ∑ u ∈ I', onIocAux f u
⊢ Set.Ioc u' v ∉ I'
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 α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun i ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun i ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun i ↦ ⋃ j, ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬μ W = 0
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (fun j ↦ μ (W ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : ℕ → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun j ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun j ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
h₃ : ∀ᶠ (j : ℕ) in atTop, Disjoint (b j) (W ∩ B j)
h₄ : ∀ᶠ (j : ℕ) in atTop, μ (B j) ≤ ↑C * μ (b j)
j : ℕ
hB : ↑C⁻¹ * μ (B j) ≠ ∞
hj₁ : Disjoint (b j) (W ∩ B j)
hj₂ : μ (B j) ≤ ↑C * μ (b j)
⊢ μ (B j) / ↑C ≤ μ (b j)

Tactic:
exact ENNReal.div_le_of_le_mul' hj₂

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
⊢ ∃ M, eLpNormEssSup ({x | M ≤ ↑‖f x‖₊}.indicator f) μ = 0

Tactic:
refine ⟨(eLpNorm f ∞ μ + 1).toReal, ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
⊢ eLpNormEssSup ({x | (eLpNorm f ∞ μ + 1).toReal ≤ ↑‖f x‖₊}.indicator f) μ = 0
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 : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
this :
  ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      blimsup (fun i ↦ cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ cthickening (r i) (s i)) atTop p
r' : ℕ → ℝ := fun i ↦ if 0 < r i then r i else 1 / (↑i + 1)
hr' : Tendsto r' atTop (𝓝[>] 0)
h₀ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i)
h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)
h₂ : ∀ (i : ℕ), p i ∧ r i ≤ 0 → cthickening (M * r i) (s i) = cthickening (r i) (s i)
⊢ p = fun i ↦ p i ∧ 0 < r i ∨ p i ∧ r i ≤ 0

Tactic:
ext i

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 : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
this :
  ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      blimsup (fun i ↦ cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ cthickening (r i) (s i)) atTop p
r' : ℕ → ℝ := ⋯
hr' : Tendsto r' atTop (𝓝[>] 0)
h₀ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i)
h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)
h₂ : ∀ (i : ℕ), p i ∧ r i ≤ 0 → cthickening (M * r i) (s i) = cthickening (r i) (s i)
i : ℕ
⊢ p i ↔ p i ∧ 0 < r i ∨ p i ∧ r i ≤ 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
⊢ toENNRealVectorMeasure 0 = 0

Tactic:
ext i

Goal state after:
α : Type u_1
m : MeasurableSpace α
i : Set α
a✝ : MeasurableSet i
⊢ (toENNRealVectorMeasure 0) i = 0 i
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
⊢ eLpNorm f p (μ.restrict s) ≤ ENNReal.ofReal ε

Tactic:
refine le_trans (eLpNorm_le_of_ae_bound haebdd) ?_

Goal state after:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M
⊢ (μ.restrict s) univ ^ p.toReal⁻¹ * ENNReal.ofReal M ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
s : Set α
x : α
m : M
hs : MeasurableSet s
inst✝ : Decidable (x ∈ s)
⊢ (dirac x m).restrict s = if x ∈ s then dirac x m else 0

Tactic:
by
  classical
  ext t ht
  simp only [hs, ht, restrict_apply]
  split_ifs with has <;> simp [dirac, ht, ht.inter hs, has]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : ¬Measurable f
⊢ 0 = c • 0

Tactic:
ext i

Goal state after:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : ¬Measurable f
i : Set β
a✝ : MeasurableSet i
⊢ 0 i = (c • 0) i
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
⊢ toSignedMeasure 0 = 0

Tactic:
by
  ext1 i hi
  rw [toSignedMeasure, toSignedMeasure_sub_apply hi, zero_posPart, zero_negPart, sub_self,
    FunLike.coe_zero, Pi.zero_apply]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : j.posPart S = 0
hS₃ : j.negPart Sᶜ = 0
⊢ ∃ S, MeasurableSet S ∧ j.toSignedMeasure ≤[S] 0 ∧ 0 ≤[Sᶜ] j.toSignedMeasure ∧ j.posPart S = 0 ∧ j.negPart Sᶜ = 0

Tactic:
refine ⟨S, hS₁, ?_, ?_, hS₂, hS₃⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : j.posPart S = 0
hS₃ : j.negPart Sᶜ = 0
⊢ j.toSignedMeasure ≤[S] 0

case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : j.posPart S = 0
hS₃ : j.negPart Sᶜ = 0
⊢ 0 ≤[Sᶜ] j.toSignedMeasure
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
⊢ μ.toSignedMeasure.toMeasureOfZeroLE univ ⋯ ⋯ = μ

Tactic:
refine Measure.ext fun i hi => ?_
  lift μ i to ℝ≥0 using (measure_lt_top _ _).ne with m hm
  rw [SignedMeasure.toMeasureOfZeroLE_apply _ _ _ hi, ENNReal.coe_inj]
  congr
  simp [hi, ← hm, measureReal_def]

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : MeasurableSpace Ω'
inst✝⁴ : TopologicalSpace Ω
inst✝³ : TopologicalSpace Ω'
inst✝² : BorelSpace Ω
inst✝¹ : BorelSpace Ω'
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
μ : FiniteMeasure Ω'
hμ : μ ∈ {μ | μ (range f)ᶜ = 0}
g : Ω →ᵇ ℝ
g' : Ω' →ᵇ ℝ
hg' : ⇑g' ∘ f = ⇑g
⊢ Tendsto (fun i ↦ ∫ (x : Ω), g x ∂↑(comap f i)) (𝓝[{μ | μ (range f)ᶜ = 0}] μ) (𝓝 (∫ (x : Ω), g x ∂↑(comap f μ)))

Tactic:
have A x : g x = g' (f x) := by change (⇑g) x = (⇑g' ∘ f) x; simp only [hg']

Goal state after:
Ω : Type u_1
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : MeasurableSpace Ω'
inst✝⁴ : TopologicalSpace Ω
inst✝³ : TopologicalSpace Ω'
inst✝² : BorelSpace Ω
inst✝¹ : BorelSpace Ω'
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
μ : FiniteMeasure Ω'
hμ : μ ∈ {μ | μ (range f)ᶜ = 0}
g : Ω →ᵇ ℝ
g' : Ω' →ᵇ ℝ
hg' : ⇑g' ∘ f = ⇑g
A : ∀ (x : Ω), g x = g' (f x)
⊢ Tendsto (fun i ↦ ∫ (x : Ω), g x ∂↑(comap f i)) (𝓝[{μ | μ (range f)ᶜ = 0}] μ) (𝓝 (∫ (x : Ω), g x ∂↑(comap f μ)))
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
h_meas : ∀ i ∈ S, setsΩ i ∈ (fun x ↦ {s | MeasurableSet s}) i
setsβ : (i : ι) → Set (β i) := fun i ↦ if hi_mem : i ∈ S then Exists.choose ⋯ else univ
⊢ ∀ i ∈ S, MeasurableSet (setsβ i)

Tactic:
intro i hi_mem

Goal state after:
α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
h_meas : ∀ i ∈ S, setsΩ i ∈ (fun x ↦ {s | MeasurableSet s}) i
setsβ : (i : ι) → Set (β i) := fun i ↦ if hi_mem : i ∈ S then Exists.choose ⋯ else univ
i : ι
hi_mem : i ∈ S
⊢ MeasurableSet (setsβ i)
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s : Set Ω
⊢ IndepSet s ∅ κ μ

Tactic:
simp only [IndepSet, generateFrom_singleton_empty]

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s : Set Ω
⊢ Indep (generateFrom {s}) ⊥ κ μ
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
h_meas : ∀ i ∈ S, setsΩ i ∈ (fun x ↦ {s | MeasurableSet s}) i
setsβ : (i : ι) → Set (β i) := fun i ↦ if hi_mem : i ∈ S then Exists.choose ⋯ else univ
h_measβ : ∀ i ∈ S, MeasurableSet (setsβ i)
⊢ ∀ i ∈ S, setsΩ i = f i ⁻¹' setsβ i

Tactic:
intro i hi_mem

Goal state after:
α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
h_meas : ∀ i ∈ S, setsΩ i ∈ (fun x ↦ {s | MeasurableSet s}) i
setsβ : (i : ι) → Set (β i) := fun i ↦ if hi_mem : i ∈ S then Exists.choose ⋯ else univ
h_measβ : ∀ i ∈ S, MeasurableSet (setsβ i)
i : ι
hi_mem : i ∈ S
⊢ setsΩ i = f i ⁻¹' setsβ i
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s t : Set Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t
s1 t1 : Set Ω
hs1 : s1 ∈ {s}
ht1 : t1 ∈ {t}
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (s1 ∩ t1) = (κ a) s1 * (κ a) t1

Tactic:
Set.mem_singleton_iff.mp hs1,

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s t : Set Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t
s1 t1 : Set Ω
hs1 : s1 ∈ {s}
ht1 : t1 ∈ {t}
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t1) = (κ a) s * (κ a) t1
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
f : ℕ → Set Ω
hfd : Pairwise (Function.onFun Disjoint f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
a : α
ha : ∀ (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
⊢ ∑' (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * ∑' (i : ℕ), (κ a) (f i)

Tactic:
simp only [ENNReal.tsum_mul_left, ha]

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

Goal state before:
pp: case mp
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsZeroOrMarkovKernel κ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set β'
h : ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)
hs : MeasurableSet s
ht : MeasurableSet t
⊢ IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ

Tactic:
indepSet_iff_measure_inter_eq_mul (hf hs) (hg ht) κ μ

Goal state after:
case mp
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsZeroOrMarkovKernel κ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set β'
h : ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst✝¹ : MeasurableSpace 𝓧
inst✝ : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
⊢ (fun ω ↦ X ω.1) ⟂ᵢ[μ.prod ν] fun ω ↦ Y ω.2

Tactic:
have : (fun ω ↦ mX.mk X ω.1) ⟂ᵢ[μ.prod ν] (fun ω ↦ mY.mk Y ω.2) :=
    indepFun_prod mX.measurable_mk mY.measurable_mk
  refine this.congr ?_ ?_
  · rw [← Function.comp_def, ← Function.comp_def]
    apply ae_eq_comp
    · exact measurable_fst.aemeasurable
    · rw [measurePreserving_fst.map_eq]
      exact (AEMeasurable.ae_eq_mk mX).symm
  · rw [← Function.comp_def, ← Function.comp_def]
    apply ae_eq_comp
    · exact measurable_snd.aemeasurable
    · rw [measurePreserving_snd.map_eq]
      exact (AEMeasurable.ae_eq_mk mY).symm

Goal state after:
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
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → μ (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, μ (f i ⁻¹' sets i)
this : IsProbabilityMeasure μ
h₀ :
  ∀ {s : (i : ι) → Set (β i)},
    (∀ (i : ι), MeasurableSet (s i)) →
      ∏ i, μ (f i ⁻¹' s i) = ∏ i, (Measure.map (f i) μ) (s i) ∧
        μ (⋂ i, f i ⁻¹' s i) = (Measure.map (fun ω i ↦ f i ω) μ) (univ.pi s)
⊢ Measure.map (fun ω i ↦ f i ω) μ = Measure.pi fun i ↦ Measure.map (f i) μ

Tactic:
refine (Measure.pi_eq fun h' hm ↦ ?_).symm

Goal state after:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → μ (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, μ (f i ⁻¹' sets i)
this : IsProbabilityMeasure μ
h₀ :
  ∀ {s : (i : ι) → Set (β i)},
    (∀ (i : ι), MeasurableSet (s i)) →
      ∏ i, μ (f i ⁻¹' s i) = ∏ i, (Measure.map (f i) μ) (s i) ∧
        μ (⋂ i, f i ⁻¹' s i) = (Measure.map (fun ω i ↦ f i ω) μ) (univ.pi s)
h' : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (h' i)
⊢ (Measure.map (fun ω i ↦ f i ω) μ) (univ.pi h') = ∏ i, (Measure.map (f i) μ) (h' i)
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
hf : ∀ (i : ι), AEMeasurable (f i) μ
h : iIndepFun f μ
⊢ Measure.map (fun ω i ↦ f i ω) μ = Measure.pi fun i ↦ Measure.map (f i) μ

Tactic:
by
  have := h.isProbabilityMeasure
  rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at h
  have h₀ {s : ∀ i, Set (β i)} (hm : ∀ (i : ι), MeasurableSet (s i)) :
      ∏ i : ι, μ (f i ⁻¹' s i) = ∏ i : ι, μ.map (f i) (s i) ∧
      μ (⋂ i : ι, (f i ⁻¹' s i)) = μ.map (fun ω i ↦ f i ω) (univ.pi s) := by
    constructor
    · congr with x
      rw [Measure.map_apply_of_aemeasurable (hf x) (hm x)]
    · rw [Measure.map_apply_of_aemeasurable (aemeasurable_pi_lambda _ fun x ↦ hf x)
        (.univ_pi hm)]
      congr with x
      simp
  refine (Measure.pi_eq fun h' hm ↦ ?_).symm
  rw [← (h₀ hm).1, ← (h₀ hm).2]
  simpa [hm] using h Finset.univ (sets := h')

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᵐ[volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
this : (fun x ↦ ‖f x‖ₑ * g x) =ᵐ[volume] fun x ↦ ‖f x * (pdf X ℙ volume x).toReal‖ₑ
⊢ ∫⁻ (a : ℝ), ‖f a * (pdf X ℙ volume a).toReal‖ₑ < ∞

Tactic:
lt_top_iff_ne_top,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᵐ[volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
this : (fun x ↦ ‖f x‖ₑ * g x) =ᵐ[volume] fun x ↦ ‖f x * (pdf X ℙ volume x).toReal‖ₑ
⊢ ∫⁻ (a : ℝ), ‖f a * (pdf X ℙ volume a).toReal‖ₑ ≠ ∞
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
inst✝ : MeasurableSingletonClass Ω
x : Ω
⊢ AEMeasurable X (Measure.dirac x)

Tactic:
exact aemeasurable_dirac

Goal state after: