mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a✝ : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : β
⊢ (η (a✝, a)) (Prod.mk a ⁻¹' s ×ˢ t) = s.indicator (fun b ↦ (η (a✝, b)) t) a

Tactic:
by_cases ha : a ∈ s

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a✝ : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : β
ha : a ∈ s
⊢ (η (a✝, a)) (Prod.mk a ⁻¹' s ×ˢ t) = s.indicator (fun b ↦ (η (a✝, b)) t) a

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a✝ : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : β
ha : a ∉ s
⊢ (η (a✝, a)) (Prod.mk a ⁻¹' s ×ˢ t) = s.indicator (fun b ↦ (η (a✝, b)) t) a
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case inr.refine_4.e_a
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
x : α
⊢ ENNReal.ofReal ((rexp (f x))⁻¹ / (∫ (x : α), rexp (f x) ∂ν)⁻¹) =
    ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν)

pp: case inr.refine_4.e_a
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
x : α
⊢ 0 < rexp (f x) / ∫ (x : α), rexp (f x) ∂ν

Tactic:
← exp_neg,

Goal state after:
case inr.refine_4.e_a
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
x : α
⊢ ENNReal.ofReal (rexp (-f x) / (∫ (x : α), rexp (f x) ∂ν)⁻¹) = ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν)

case inr.refine_4.e_a
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
x : α
⊢ 0 < rexp (f x) / ∫ (x : α), rexp (f x) ∂ν
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: case pos
x : ℝ
h0 : x = 0
⊢ derivWithin klFun (Iio x) x = log x

pp: case neg
x : ℝ
h0 : ¬x = 0
⊢ derivWithin klFun (Iio x) x = log x

Tactic:
· simp only [h0, log_zero]
    exact derivWithin_zero_of_not_differentiableWithinAt not_differentiableWithinAt_klFun_Iio_zero

Goal state after:
case neg
x : ℝ
h0 : ¬x = 0
⊢ derivWithin klFun (Iio x) x = log x
Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp

Goal state before:
pp: case inl
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
inst✝ : Nontrivial ↥(Lp E ∞ μ)
f : ↥(Lp E ∞ μ)
hf : f ≠ 0
hfne : MemLp.toLp (fun x ↦ 1) ⋯ = 0
this : ↑↑(MemLp.toLp (fun x ↦ 1) ⋯) =ᵐ[μ] 0
⊢ ↑↑f =ᵐ[μ] 0

Tactic:
MemLp.coeFn_toLp

Goal state after:
case inl
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
inst✝ : Nontrivial ↥(Lp E ∞ μ)
f : ↥(Lp E ∞ μ)
hf : f ≠ 0
hfne : MemLp.toLp (fun x ↦ 1) ⋯ = 0
this : (fun x ↦ 1) =ᵐ[μ] 0
⊢ ↑↑f =ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp

Goal state before:
pp: case inr.inl
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
inst✝ : Nontrivial ↥(Lp E 0 μ)
f : ↥(Lp E 0 μ)
hf : f ≠ 0
h'p : 0 < ∞
this✝ : MemLp (fun x ↦ 1) 0 μ
hfne : MemLp.toLp (fun x ↦ 1) this✝ = 0
this : ↑↑(MemLp.toLp (fun x ↦ 1) this✝) =ᵐ[μ] 0
⊢ ↑↑f =ᵐ[μ] 0

Tactic:
MemLp.coeFn_toLp

Goal state after:
case inr.inl
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
inst✝ : Nontrivial ↥(Lp E 0 μ)
f : ↥(Lp E 0 μ)
hf : f ≠ 0
h'p : 0 < ∞
this✝ : MemLp (fun x ↦ 1) 0 μ
hfne : MemLp.toLp (fun x ↦ 1) this✝ = 0
this : (fun x ↦ 1) =ᵐ[μ] 0
⊢ ↑↑f =ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedSpace ℝ E
hp : Fact (1 ≤ p)
inst✝¹ : CompleteSpace ↥(Lp E p μ)
inst✝ : Nontrivial ↥(Lp E p μ)
f : ↥(Lp ℝ p μ)
m : E →L[ℝ] ↥(Lp E p μ) := ⋯
u : ℕ → E
hu : CauchySeq u
g : ↥(Lp E p μ)
hg : Tendsto (⇑m ∘ u) atTop (𝓝 g)
f' : ℕ → α → E := ⋯
ns : ℕ → ℕ
hns : StrictMono ns
nslim : ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f' (ns i) x) atTop (𝓝 (↑↑g x))
hf : ↑↑f =ᵐ[μ] 0
⊢ ↑↑f =ᵐ[μ] ↑↑0

Tactic:
grw [Lp.coeFn_zero]

Goal state after:
α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedSpace ℝ E
hp : Fact (1 ≤ p)
inst✝¹ : CompleteSpace ↥(Lp E p μ)
inst✝ : Nontrivial ↥(Lp E p μ)
f : ↥(Lp ℝ p μ)
m : E →L[ℝ] ↥(Lp E p μ) := (compLpL₂ p μ (lsmul ℝ ℝ).flip).flip f
u : ℕ → E
hu : CauchySeq u
g : ↥(Lp E p μ)
hg : Tendsto (⇑m ∘ u) atTop (𝓝 g)
f' : ℕ → α → E := fun n ↦ ↑↑((⇑m ∘ u) n)
ns : ℕ → ℕ
hns : StrictMono ns
nslim : ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f' (ns i) x) atTop (𝓝 (↑↑g x))
hf : ↑↑f =ᵐ[μ] 0
⊢ ↑↑f =ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedSpace ℝ E
hp : Fact (1 ≤ p)
inst✝¹ : CompleteSpace ↥(Lp E p μ)
inst✝ : Nontrivial ↥(Lp E p μ)
f : ↥(Lp ℝ p μ)
hf : f ≠ 0
m : E →L[ℝ] ↥(Lp E p μ) := (compLpL₂ p μ (lsmul ℝ ℝ).flip).flip f
u : ℕ → E
hu : CauchySeq u
g : ↥(Lp E p μ)
hg : Tendsto (⇑m ∘ u) atTop (𝓝 g)
f' : ℕ → α → E := fun n ↦ ↑↑((⇑m ∘ u) n)
ns : ℕ → ℕ
hns : StrictMono ns
nslim : ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f' (ns i) x) atTop (𝓝 (↑↑g x))
this : (ae (μ.restrict (Function.support ↑↑f))).NeBot
A : ∀ᵐ (x : α) ∂μ.restrict (Function.support ↑↑f), Tendsto (fun i ↦ f' (ns i) x) atTop (𝓝 (↑↑g x))
B : ∀ᵐ (x : α) ∂μ.restrict (Function.support ↑↑f), x ∈ Function.support ↑↑f
n : ℕ
x : α
hx : ↑↑((toSpanSingleton ℝ (u n)).compLp f) x = (toSpanSingleton ℝ (u n)) (↑↑f x)
⊢ ↑↑(m (u n)) x = ↑↑f x • u n

Tactic:
simp [m, hx]

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : ¬c = 0
hc' : ↑c ≠ 0
hμ_smul : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr (c • μ) (c • ν)) (c • μ)
⊢ Integrable (llr (c⁻¹ • c • μ) (c⁻¹ • c • ν)) (c • μ)

Tactic:
integrable_congr (llr_smul_nnreal_same (hμν.smul c) c⁻¹ (by simpa))

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : ¬c = 0
hc' : ↑c ≠ 0
hμ_smul : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr (c • μ) (c • ν)) (c • μ)
⊢ Integrable (llr (c • μ) (c • ν)) (c • μ)
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
⊢ μ = 0

Tactic:
hν

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ 0
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
⊢ μ = 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable

Goal state before:
pp: α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
one_le_p : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
f : α → F
hf : MemLp f p (μ.trim hm)
⊢ f =ᵐ[μ] ↑↑(MemLp.toLp f ⋯)

Tactic:
MemLp.coeFn_toLp

Goal state after:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
one_le_p : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
f : α → F
hf : MemLp f p (μ.trim hm)
⊢ f =ᵐ[μ] f
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_2
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E'
h_ae_eq_f : ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑f a⟫) ⋯) =ᵐ[μ] fun a ↦ ⟪c, ↑↑f a⟫
⊢ ∫ (x : α) in s, ↑↑↑((condExpL2 𝕜 𝕜 hm) (MemLp.toLp (fun a ↦ ⟪c, ↑↑f a⟫) ⋯)) x ∂μ =
    ∫ (x : α) in s, ↑↑(MemLp.toLp (fun a ↦ ⟪c, ↑↑f a⟫) ⋯) x ∂μ

Tactic:
exact integral_condExpL2_eq_of_fin_meas_real _ hs hμs

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

Goal state before:
pp: α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : InnerProductSpace 𝕜 E'
inst✝² : CompleteSpace E'
inst✝¹ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E'
⊢ Integrable (↑↑↑((condExpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x))) μ

Tactic:
refine integrable_of_forall_fin_meas_le' hm (μ s * ‖x‖₊)
    (ENNReal.mul_lt_top hμs.lt_top ENNReal.coe_lt_top) ?_ ?_

Goal state after:
case refine_1
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : InnerProductSpace 𝕜 E'
inst✝² : CompleteSpace E'
inst✝¹ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E'
⊢ AEStronglyMeasurable (↑↑↑((condExpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x))) μ

case refine_2
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : InnerProductSpace 𝕜 E'
inst✝² : CompleteSpace E'
inst✝¹ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E'
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      μ s_1 ≠ ∞ → ∫⁻ (x_1 : α) in s_1, ‖↑↑↑((condExpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x)) x_1‖ₑ ∂μ ≤ μ s * ↑‖x‖₊
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : G
⊢ Integrable (↑↑(condExpIndSMul hm hs hμs x)) μ

Tactic:
refine integrable_of_forall_fin_meas_le' hm (μ s * ‖x‖₊)
    (ENNReal.mul_lt_top hμs.lt_top ENNReal.coe_lt_top) ?_ ?_

Goal state after:
case refine_1
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : G
⊢ AEStronglyMeasurable (↑↑(condExpIndSMul hm hs hμs x)) μ

case refine_2
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : G
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 → μ s_1 ≠ ∞ → ∫⁻ (x_1 : α) in s_1, ‖↑↑(condExpIndSMul hm hs hμs x) x_1‖ₑ ∂μ ≤ μ s * ↑‖x‖₊
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: case refine_1
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : CompleteSpace F'
f : ↥(lpMeas F' ℝ m 1 μ)
g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm) f
hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g
c : F'
s : Set α
hs : MeasurableSet s
hμs : (μ.trim hm) s < ∞
⊢ (condExpL1CLM F' hm μ) (indicatorConstLp 1 ⋯ ⋯ c) = indicatorConstLp 1 ⋯ ⋯ c

Tactic:
condExpL1CLM_indicatorConstLp

Goal state after:
case refine_1
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : CompleteSpace F'
f : ↥(lpMeas F' ℝ m 1 μ)
g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm) f
hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g
c : F'
s : Set α
hs : MeasurableSet s
hμs : (μ.trim hm) s < ∞
⊢ (condExpInd F' hm μ s) c = indicatorConstLp 1 ⋯ ⋯ c
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
ι : Type u_5
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[fun a ↦ ∑' (i : ι), f i a | m] =ᵐ[μ] fun a ↦ ∑' (i : ι), μ[f i | m] a

Tactic:
simp only [condExp_of_not_sigmaFinite hm hμm, Pi.zero_apply, tsum_zero]
    exact ae_eq_rfl

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

Goal state before:
pp: case pos
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
hX : Measurable X
⊢ Measurable P⁻[X | mΩ]

pp: case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
hX : ¬Measurable X
⊢ Measurable P⁻[X | mΩ]

Tactic:
· simp [condLExp_eq_self hm, hX]

Goal state after:
case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
hX : ¬Measurable X
⊢ Measurable P⁻[X | mΩ]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
⊢ ∫ (x : α) in sᶜ, μ[s.indicator f | m] x ∂μ.restrict t = 0

Tactic:
Measure.restrict_restrict (MeasurableSet.compl (hm _ hs_m))

Goal state after:
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
⊢ ∫ (x : α) in sᶜ ∩ t, μ[s.indicator f | m] x ∂μ = 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
hm : m ≤ m𝓧
μ : Measure 𝓧
inst✝ : SigmaFinite (μ.trim hm)
s : Set 𝓧
hs : MeasurableSet s
h's : μ s ≠ ∞
⊢ Integrable (s.indicator 1) μ

pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
hm : m ≤ m𝓧
μ : Measure 𝓧
inst✝ : SigmaFinite (μ.trim hm)
s : Set 𝓧
hs : MeasurableSet s
h's : μ s ≠ ∞
⊢ 0 ≤ᵐ[μ] s.indicator 1

Tactic:
· apply (integrable_indicator_iff hs).2
      apply integrableOn_const h's

Goal state after:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
hm : m ≤ m𝓧
μ : Measure 𝓧
inst✝ : SigmaFinite (μ.trim hm)
s : Set 𝓧
hs : MeasurableSet s
h's : μ s ≠ ∞
⊢ 0 ≤ᵐ[μ] s.indicator 1
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
inst✝¹ : FiniteDimensional ℝ E
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ univ φ
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
⊢ μ[φ ∘ f | m] ≤ᵐ[μ] φ ∘ μ[f | m]

Tactic:
filter_upwards [hφ_cvx.neg.map_condExp_le_of_finiteDimensional hm hf_int hφ_int.neg,
    condExp_neg (φ ∘ f) m] with a h ha

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
inst✝¹ : FiniteDimensional ℝ E
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ univ φ
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
a : α
h : ((-φ) ∘ μ[f | m]) a ≤ μ[(-φ) ∘ f | m] a
ha : μ[-φ ∘ f | m] a = (-μ[φ ∘ f | m]) a
⊢ μ[φ ∘ f | m] a ≤ (φ ∘ μ[f | m]) a
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case refine_3
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsOrderedRing k
n : ℕ
i : Fin n
x : k
hxpos : 0 < x
hx1 : x ≤ 1
w : Fin n → k
hw : ∑ i, w i = 1
hi : w i = 1 - x
hj : ∀ (j : Fin n), j ≠ i → x⁻¹ * w j ∈ Set.Icc 0 1
⊢ ∀ (j : Fin n), w j ∈ Set.Icc 0 1

Tactic:
suffices ∀ j, 0 ≤ w j from
      fun j ↦ ⟨this j, hw ▸ Finset.single_le_sum (fun j _ ↦ this j) (mem_univ j)⟩
    intro j
    by_cases hji : j = i <;> aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x ↦ Mᵢ) N₁
b : MultilinearMap R' (fun x ↦ Mᵢ) N₂
σ : Perm (ιa ⊕ ιb)
f : Perm ιa × Perm ιb →* Perm (ιa ⊕ ιb) := sumCongrHom ιa ιb
⊢ ∑ x with x ∈ (sumCongrHom ιa ιb).range, sign (σ * x) • domDomCongr (σ * x) (a.domCoprod b) =
    ∑ x, sign (σ * (sumCongrHom ιa ιb) x) • domDomCongr (σ * (sumCongrHom ιa ιb) x) (a.domCoprod b)

Tactic:
MonoidHom.mem_range,

Goal state after:
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x ↦ Mᵢ) N₁
b : MultilinearMap R' (fun x ↦ Mᵢ) N₂
σ : Perm (ιa ⊕ ιb)
f : Perm ιa × Perm ιb →* Perm (ιa ⊕ ιb) := sumCongrHom ιa ιb
⊢ ∑ x with ∃ x_1, (sumCongrHom ιa ιb) x_1 = x, sign (σ * x) • domDomCongr (σ * x) (a.domCoprod b) =
    ∑ x, sign (σ * (sumCongrHom ιa ιb) x) • domDomCongr (σ * (sumCongrHom ιa ιb) x) (a.domCoprod b)
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
hcomm : ∀ (i j : ι), i ≠ j → ∀ (r : R), r • f (b j) = (b.coord i) (f (b i)) • r • b j
i j : ι
⊢ (b.coord i) (f (b i)) = (b.coord j) (f (b j))

Tactic:
by_cases hij : j = i

Goal state after:
case pos
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
hcomm : ∀ (i j : ι), i ≠ j → ∀ (r : R), r • f (b j) = (b.coord i) (f (b i)) • r • b j
i j : ι
hij : j = i
⊢ (b.coord i) (f (b i)) = (b.coord j) (f (b j))

case neg
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
hcomm : ∀ (i j : ι), i ≠ j → ∀ (r : R), r • f (b j) = (b.coord i) (f (b i)) • r • b j
i j : ι
hij : ¬j = i
⊢ (b.coord i) (f (b i)) = (b.coord j) (f (b j))
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
i j : ι
hij : i ≠ j
r : R
x : V := b.repr.symm ((Finsupp.single i 1).update j r)
s t : R
hst : s = 0 → ¬t = 0
h : ∀ (i : ι), s * (b.repr x) i + t * (b.repr (f x)) i = 0
hx : x = b i + r • b j
h1 : s + t * (b.coord i) (f (b i)) = 0
this : s * r + t * ((b.repr (f (b i))) j + r * (b.repr (f (b j))) j) = 0
⊢ s * r + t * r * (b.coord j) (f (b j)) = 0

Tactic:
rw [mul_add, ← add_assoc, add_right_comm, add_eq_zero_iff_eq_neg, ← mul_assoc] at this
        rw [Basis.coord_apply, this, feq]
        simp [single_eq_of_ne' hij]

Goal state after:
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
i j : ι
hij : i ≠ j
r : R
x : V := b.repr.symm ((Finsupp.single i 1).update j r)
s t : R
hst : s = 0 → ¬t = 0
h : ∀ (i : ι), s * (b.repr x) i + t * (b.repr (f x)) i = 0
hx : x = b i + r • b j
h1 : s = -(t * (b.coord i) (f (b i)))
h2 : t * (r * (b.coord j) (f (b j))) - t * ((b.coord i) (f (b i)) * r) = 0
⊢ (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))

Tactic:
← mul_sub,

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
i j : ι
hij : i ≠ j
r : R
x : V := b.repr.symm ((Finsupp.single i 1).update j r)
s t : R
hst : s = 0 → ¬t = 0
h : ∀ (i : ι), s * (b.repr x) i + t * (b.repr (f x)) i = 0
hx : x = b i + r • b j
h1 : s = -(t * (b.coord i) (f (b i)))
h2 : t * (r * (b.coord j) (f (b j)) - (b.coord i) (f (b i)) * r) = 0
⊢ (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
z : A
v : V
⊢ (ofBaseChange A Q) (z ⊗ₜ[R] (ι Q) v) = (ι (QuadraticForm.baseChange A Q)) (z ⊗ₜ[R] v)

Tactic:
change algebraMap _ _ z * ofBaseChangeAux A Q (ι Q v) = ι (Q.baseChange A) (z ⊗ₜ[R] v)

Goal state after:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
z : A
v : V
⊢ (algebraMap A (CliffordAlgebra (QuadraticForm.baseChange A Q))) z * (ofBaseChangeAux A Q) ((ι Q) v) =
    (ι (QuadraticForm.baseChange A Q)) (z ⊗ₜ[R] v)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx : (contractLeft d) ((contractLeft d') x✝) = -(contractLeft d') ((contractLeft d) x✝)
⊢ d' m✝ • (contractLeft d) x✝ - (d m✝ • (contractLeft d') x✝ - (ι Q) m✝ * (contractLeft d) ((contractLeft d') x✝)) =
    -(d m✝ • (contractLeft d') x✝ - (d' m✝ • (contractLeft d) x✝ - (ι Q) m✝ * (contractLeft d') ((contractLeft d) x✝)))

Tactic:
rw [neg_sub, sub_sub_eq_add_sub, hx, mul_neg, ← sub_eq_add_neg]

Goal state after: