mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsFiniteKernel η
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
s : Set 𝓧
hs : MeasurableSet s
⊢ μ s < ∞ → ∫⁻ (x : 𝓧) in s, ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (x, b) ∂η x ∂μ = ∫⁻ (x : 𝓧) in s, (κ x) univ ∂μ

Tactic:
hsμ

Goal state after:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsFiniteKernel η
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
s : Set 𝓧
hs : MeasurableSet s
hsμ : μ s < ∞
⊢ ∫⁻ (x : 𝓧) in s, ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (x, b) ∂η x ∂μ = ∫⁻ (x : 𝓧) in s, (κ x) univ ∂μ
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Kernel α β
κ η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : ¬IsSFiniteKernel μ
⊢ μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η

pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Kernel α β
κ η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : IsSFiniteKernel μ
⊢ μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η

Tactic:
· simp [hμ]

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 η
hμ : IsSFiniteKernel μ
⊢ μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : ¬AEMeasurable f μ
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ

Tactic:
· have hf' : ¬ Integrable (fun x ↦ exp (f x)) μ := by
      exact fun h ↦ hf (aemeasurable_of_aemeasurable_exp h.1.aemeasurable)
    simp only [hf, not_false_eq_true, tilted_of_not_aemeasurable, Measure.restrict_zero,
      lintegral_zero_measure]
    rw [integral_undef hf']
    simp

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

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
⊢ (∫ (x : α) in s, g x ∂μ.withDensity fun x ↦ ↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯)) =
    ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ

Tactic:
setIntegral_withDensity_eq_setIntegral_smul₀ _ _ hs

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
⊢ ∫ (x : α) in s, NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯ • g x ∂μ =
    ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ

α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
⊢ AEMeasurable (fun x ↦ NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) (μ.restrict s)
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: case hx
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : (c • μ).rnDeriv ν =ᵐ[ν] c • μ.rnDeriv ν
x : α
hx_eq : (c • μ).rnDeriv ν x = (c • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ c ≠ 0 ∧ c ≠ ∞

Tactic:
simp [hc, hc_ne_top]

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

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → E
hμ : μ = 0
⊢ Integrable g (μ.tilted f) ↔ Integrable (fun x ↦ rexp (f x) • g x) μ

pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
⊢ Integrable g (μ.tilted f) ↔ Integrable (fun x ↦ rexp (f x) • g x) μ

Tactic:
· simp [hμ]

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
⊢ Integrable g (μ.tilted f) ↔ Integrable (fun x ↦ rexp (f x) • g x) μ
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: case hx
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : μ.rnDeriv (c • ν) =ᵐ[ν] c⁻¹ • μ.rnDeriv ν
x : α
hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ c⁻¹ ≠ 0 ∧ c⁻¹ ≠ ∞

Tactic:
simp [hc, hc_ne_top]

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

Goal state before:
pp: case mp
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ klDiv μ ν ≠ ∞

Tactic:
simp [klDiv_of_ac_of_integrable h.1 h.2]

Goal state after:
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 α
hm : m ≤ m0
⊢ Function.RightInverse (lpTrimToLpMeasSubgroup F p μ hm) (lpMeasSubgroupToLpTrim F p μ hm)

Tactic:
by
  intro f
  ext1
  refine
    (Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm (Lp.stronglyMeasurable _) ?_
  exact (lpMeasSubgroupToLpTrim_ae_eq hm _).trans (lpTrimToLpMeasSubgroup_ae_eq hm _)

Goal state after:
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
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ

pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ

Tactic:
· simp [hμ]

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
⊢ ↑↑0 =ᵐ[μ] ↑↑(0 x)

Tactic:
zero_apply,

Goal state after:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
⊢ ↑↑0 =ᵐ[μ] ↑↑0
Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
p : 𝓧 × 𝓨
⊢ (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p →
    ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal =
      ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)

Tactic:
hp

Goal state after:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p
⊢ ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal =
    ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᵐ[μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f | m] =ᵐ[μ] μ[g | m]

Tactic:
simp_rw [condExp_of_not_sigmaFinite hm hμm]

Goal state after:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : f =ᵐ[μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ 0 =ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ ∫ (x : α), μ[f | m] x ∂μ = ∫ (x : α), f x ∂μ

Tactic:
by
  by_cases hf : Integrable f μ
  · suffices ∫ x in Set.univ, (μ[f | m]) x ∂μ = ∫ x in Set.univ, f x ∂μ by
      simp_rw [setIntegral_univ] at this; exact this
    exact setIntegral_condExp hm hf .univ
  simp only [condExp_of_not_integrable hf, Pi.zero_apply, integral_zero, integral_undef hf]

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f + g | m] =ᵐ[μ] μ[f | m] + μ[g | m]

Tactic:
simp_rw [condExp_of_not_sigmaFinite hm hμm]

Goal state after:
case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ 0 =ᵐ[μ] 0 + 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : m ≤ m0
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f | m] =ᵐ[μ.restrict s] 0

Tactic:
simp_rw [condExp_of_not_sigmaFinite hm hμm]

Goal state after:
case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : m ≤ m0
hμm : ¬SigmaFinite (μ.trim hm)
⊢ 0 =ᵐ[μ.restrict s] 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : α → E
m : MeasurableSpace α
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[c • f | m] =ᵐ[μ] c • μ[f | m]

Tactic:
simp_rw [condExp_of_not_sigmaFinite hm hμm]

Goal state after:
case neg
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : α → E
m : MeasurableSpace α
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ 0 =ᵐ[μ] c • 0
Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ : Kernel 𝓧 𝓨
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsMarkovKernel κ
h_ac : μ ≪ ν
p : 𝓧 × 𝓨
⊢ (∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p = (∂μ/∂ν) p.1 →
    ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p).toReal) = ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal)

Tactic:
hp

Goal state after:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ : Kernel 𝓧 𝓨
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsMarkovKernel κ
h_ac : μ ≪ ν
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p = (∂μ/∂ν) p.1
⊢ ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p).toReal) = ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal)
Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ : Kernel 𝓧 𝓨
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsMarkovKernel κ
h_ac : μ ≪ ν
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p = (∂μ/∂ν) p.1
⊢ ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p).toReal) = ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal)

Tactic:
hp

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

Goal state before:
pp: case refine_3.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
⊢ Continuous fun f ↦ (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm f)

Tactic:
refine (condExpL1CLM F' hm μ).continuous.comp (continuous_induced_dom.comp ?_)
      exact LinearIsometryEquiv.continuous _

Goal state after:
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
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := (Submodule.span ℝ t).topologicalClosure
this✝ : CompleteSpace ↥Y
this : SecondCountableTopology ↥Y
fY : α → ↥Y := fun a ↦ if h : f a ∈ Y then ⟨f a, h⟩ else 0
fX : α → E := ⇑Y.subtypeL ∘ fY
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
lem1 : f =ᵐ[μ] fX
lem2 : ∀ᵐ (a : α) ∂μ, fY a ∈ ⇑Y.subtypeL ⁻¹' s
hfY_int : Integrable fY μ
lem3 : μ[f | m] =ᵐ[μ] ⇑Y.subtypeL ∘ μ[fY | m]
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s

Tactic:
filter_upwards [(hc.linear_preimage Y.subtype).condExp_mem_of_hereditarilyLindelofSpace
    hm hfY_int (hs.preimage Y.subtypeL.continuous) lem2, lem3] with a ha hb

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := (Submodule.span ℝ t).topologicalClosure
this✝ : CompleteSpace ↥Y
this : SecondCountableTopology ↥Y
fY : α → ↥Y := fun a ↦ if h : f a ∈ Y then ⟨f a, h⟩ else 0
fX : α → E := ⇑Y.subtypeL ∘ fY
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
lem1 : f =ᵐ[μ] fX
lem2 : ∀ᵐ (a : α) ∂μ, fY a ∈ ⇑Y.subtypeL ⁻¹' s
hfY_int : Integrable fY μ
lem3 : μ[f | m] =ᵐ[μ] ⇑Y.subtypeL ∘ μ[fY | m]
a : α
ha : μ[fY | m] a ∈ ⇑Y.subtypeL ⁻¹' s
hb : μ[f | m] a = (⇑Y.subtypeL ∘ μ[fY | m]) a
⊢ μ[f | m] a ∈ s
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
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᵐ[μ] μ[gs n | m]
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f | m] =ᵐ[μ] μ[g | m]

Tactic:
simp_rw [condExp_of_not_sigmaFinite hm hμm]

Goal state after:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᵐ[μ] μ[gs n | m]
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ 0 =ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner

Goal state before:
pp: case pos.refine_3
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
s : Set 𝓧
hs : MeasurableSet s
⊢ μ s < ∞ → ∫ (x : 𝓧) in s, (μ⁻[f | m] x).toReal ∂μ = ∫ (x : 𝓧) in s, (f x).toReal ∂μ

Tactic:
hsμ

Goal state after:
case pos.refine_3
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
s : Set 𝓧
hs : MeasurableSet s
hsμ : μ s < ∞
⊢ ∫ (x : 𝓧) in s, (μ⁻[f | m] x).toReal ∂μ = ∫ (x : 𝓧) in s, (f x).toReal ∂μ
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 α
s : Set E
inst✝¹ : IsFiniteMeasure μ
inst✝ : HereditarilyLindelofSpace E
hm : m ≤ mα
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
L : ℕ → E →L[ℝ] ℝ
c : ℕ → ℝ
hLc1 : ∀ (i : ℕ), s.domRestrict ⇑(L i) + const (↑s) (c i) ≤ s.domRestrict φ
hLc2 : ⨆ i, s.domRestrict ⇑(L i) + const (↑s) (c i) = s.domRestrict φ
hp : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (fun x ↦ (L i) (μ[f | m] x) + c i) a = μ[fun y ↦ (L i) (f y) + c i | m] a
hw : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), μ[⇑(L i) ∘ f + const α (c i) | m] a ≤ μ[φ ∘ f | m] a
a : α
⊢ (∀ (i : ℕ), (L i) (μ[f | m] a) + c i = μ[fun y ↦ (L i) (f y) + c i | m] a) →
    (∀ (i : ℕ), μ[⇑(L i) ∘ f + const α (c i) | m] a ≤ μ[φ ∘ f | m] a) → μ[f | m] a ∈ s → φ (μ[f | m] a) ≤ μ[φ ∘ f | m] a

Tactic:
hp

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 α
s : Set E
inst✝¹ : IsFiniteMeasure μ
inst✝ : HereditarilyLindelofSpace E
hm : m ≤ mα
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
L : ℕ → E →L[ℝ] ℝ
c : ℕ → ℝ
hLc1 : ∀ (i : ℕ), s.domRestrict ⇑(L i) + const (↑s) (c i) ≤ s.domRestrict φ
hLc2 : ⨆ i, s.domRestrict ⇑(L i) + const (↑s) (c i) = s.domRestrict φ
hp✝ : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (fun x ↦ (L i) (μ[f | m] x) + c i) a = μ[fun y ↦ (L i) (f y) + c i | m] a
hw : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), μ[⇑(L i) ∘ f + const α (c i) | m] a ≤ μ[φ ∘ f | m] a
a : α
hp : ∀ (i : ℕ), (L i) (μ[f | m] a) + c i = μ[fun y ↦ (L i) (f y) + c i | m] a
⊢ (∀ (i : ℕ), μ[⇑(L i) ∘ f + const α (c i) | m] a ≤ μ[φ ∘ f | m] a) → μ[f | m] a ∈ s → φ (μ[f | m] a) ≤ μ[φ ∘ f | m] a
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᵐ[μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f | m] ≤ᵐ[μ] μ[g | m]

Tactic:
simp_rw [condExp_of_not_sigmaFinite hm hμm]

Goal state after:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᵐ[μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ 0 ≤ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ
hf : Integrable f μ
h'f : 0 ≤ᵐ[μ] f
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
A : μ[fun x ↦ (ENNReal.ofReal (f x)).toReal | m] =ᵐ[μ] μ[f | m]
B : 0 ≤ᵐ[μ] μ[f | m]
g : 𝓧 → ℝ≥0∞ := fun x ↦ ENNReal.ofReal (f x)
I : ∫⁻ (x : 𝓧), g x ∂μ ≠ ∞
J : ∀ᵐ (x : 𝓧) ∂μ, μ⁻[g | m] x < ∞
a : 𝓧
ha : (μ⁻[g | m] a).toReal = μ[fun x ↦ (g x).toReal | m] a
h'a : 0 a ≤ f a
h''a : μ[fun x ↦ (ENNReal.ofReal (f x)).toReal | m] a = μ[f | m] a
⊢ 0 a ≤ μ[f | m] a → μ⁻[g | m] a < ∞ → μ⁻[fun x ↦ ENNReal.ofReal (f x) | m] a = ENNReal.ofReal (μ[f | m] a)

Tactic:
h'''a

Goal state after:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ
hf : Integrable f μ
h'f : 0 ≤ᵐ[μ] f
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
A : μ[fun x ↦ (ENNReal.ofReal (f x)).toReal | m] =ᵐ[μ] μ[f | m]
B : 0 ≤ᵐ[μ] μ[f | m]
g : 𝓧 → ℝ≥0∞ := fun x ↦ ENNReal.ofReal (f x)
I : ∫⁻ (x : 𝓧), g x ∂μ ≠ ∞
J : ∀ᵐ (x : 𝓧) ∂μ, μ⁻[g | m] x < ∞
a : 𝓧
ha : (μ⁻[g | m] a).toReal = μ[fun x ↦ (g x).toReal | m] a
h'a : 0 a ≤ f a
h''a : μ[fun x ↦ (ENNReal.ofReal (f x)).toReal | m] a = μ[f | m] a
h'''a : 0 a ≤ μ[f | m] a
⊢ μ⁻[g | m] a < ∞ → μ⁻[fun x ↦ ENNReal.ofReal (f x) | m] a = ENNReal.ofReal (μ[f | m] a)
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
i : ι
⊢ (basis b ibc) i = ε (b i)

Tactic:
simp only [basis, LinearEquiv.baseChange, Module.Basis.coe_ofRepr, LinearEquiv.trans_symm,
    LinearEquiv.symm_symm, LinearEquiv.trans_apply]
  generalize_proofs _ _ _ _ ibcRA
  have : ibcRA.equiv.symm (Finsupp.single i 1) = 1 ⊗ₜ (Finsupp.single i 1) := by
    simp [LinearEquiv.symm_apply_eq, IsBaseChange.equiv_tmul]
  simp [this, IsBaseChange.equiv_tmul]

Goal state after: