mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

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

Tactic:
fun_prop

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

Goal state before:
pp: case refine_2
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (Measure.map g ν)
this✝ : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
⊢ ∀ (s : Set 𝓧),
    MeasurableSet s →
      ν s < ∞ →
        ∫ (x : 𝓧) in s, ((Measure.map g μ).rnDeriv (Measure.map g ν) (g x)).toReal ∂ν =
          ∫ (x : 𝓧) in s, (μ.rnDeriv ν x).toReal ∂ν

Tactic:
rintro _ ⟨t, ht, rfl⟩ _
    calc ∫ x in g ⁻¹' t, ((μ.map g).rnDeriv (ν.map g) (g x)).toReal ∂ν
    _ = ∫ y in t, ((μ.map g).rnDeriv (ν.map g) y).toReal ∂(ν.map g) := by
      rw [setIntegral_map ht _ hg.aemeasurable]
      exact Measurable.aestronglyMeasurable (by fun_prop)
    _ = ∫ x in g ⁻¹' t, (μ.rnDeriv ν x).toReal ∂ν := by
      rw [Measure.setIntegral_toReal_rnDeriv (hμν.map hg),
        Measure.setIntegral_toReal_rnDeriv hμν, measureReal_def, Measure.map_apply hg ht,
        measureReal_def]

Goal state after:
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 < ∞
⊢ AEMeasurable g μ

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
a✝ : (P.trim hm) s < ∞
⊢ Measurable P⁻[X | mΩ]

Tactic:
fun_prop

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

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (Measure.map g ν)
this : SigmaFinite ν
h_ne_top1 : ∀ᵐ (x : 𝓧) ∂ν, (Measure.map g μ).rnDeriv (Measure.map g ν) (g x) ≠ ∞
h_ne_top2 : ∀ᵐ (x : 𝓧) ∂ν, ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨] x ≠ ∞
⊢ AEMeasurable (μ.rnDeriv ν) ν

Tactic:
fun_prop

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

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst✝ : SigmaFinite (Measure.map g ν)
s : Set ℝ≥0∞
hs : MeasurableSet s
⊢ Measurable ((Measure.map g μ).rnDeriv (Measure.map g ν))

Tactic:
fun_prop

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

Goal state before:
pp: case hg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst✝ : SigmaFinite (Measure.map g ν)
⊢ StronglyMeasurable ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨]

Tactic:
fun_prop

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

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

Tactic:
fun_prop

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

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst✝ : SigmaFinite (Measure.map g ν)
s : Set ℝ
hs : MeasurableSet s
⊢ Measurable fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) a).toReal

Tactic:
fun_prop

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

Goal state before:
pp: case hg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst✝ : SigmaFinite (Measure.map g ν)
⊢ StronglyMeasurable ν[fun a ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]

Tactic:
fun_prop

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

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ StronglyMeasurable fun x ↦ f ((∂Measure.map g μ/∂Measure.map g ν) x).toReal

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ AEMeasurable X (P.restrict s)

Tactic:
fun_prop

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
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
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) μ
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
φY : ↥Y → ℝ := φ ∘ ⇑Y.subtypeL
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
hfY_int : Integrable fY μ
lem2 : μ[f | m] =ᵐ[μ] ⇑Y.subtypeL ∘ μ[fY | m]
lem3 : φ ∘ f =ᵐ[μ] φY ∘ fY
⊢ ContinuousOn (⇑Y.subtypeL) (⇑Y.subtypeL ⁻¹' s)

Tactic:
fun_prop

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

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ StronglyMeasurable fun x ↦ f ((∂Measure.map g μ/∂Measure.map g ν) (g x)).toReal

Tactic:
fun_prop

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

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

Tactic:
fun_prop

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

Goal state before:
pp: case pos.hf
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hX : AEMeasurable X P
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ AEMeasurable X (P.restrict s)

Tactic:
fun_prop

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

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

Tactic:
fun_prop

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

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

Tactic:
fun_prop

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

Goal state before:
pp: case refine_4
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ Integrable ν[fun a ↦ ((∂μ/∂ν) a).toReal | MeasurableSpace.comap g m𝓨] ν

Tactic:
fun_prop

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

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

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
⊢ P⁻[c • X | mΩ] =ᵐ[P] c • P⁻[X | mΩ]

Tactic:
by
  by_cases hm : mΩ ≤ mΩ₀
  swap; · simp [condLExp_of_not_le hm]
  by_cases hσ : SigmaFinite (P.trim hm)
  swap; · simp [condLExp_of_not_sigmaFinite hm hσ]
  refine (ae_eq_condLExp _ _ _ (by fun_prop) ?_).symm
  intro s hs
  simp only [Pi.smul_apply, smul_eq_mul]
  rw [lintegral_const_mul' _ _ hc, lintegral_const_mul' _ _ hc, setLIntegral_condLExp _ _ _ hs]

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

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
hm : m ≤ m𝓧
hμν : μ ≪ ν
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ StronglyMeasurable fun x ↦ f ((∂μ.trim hm/∂ν.trim hm) x).toReal

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝ : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
⊢ Measurable (∑' (i : ι), P⁻[X i | mΩ])

Tactic:
fun_prop

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

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
hm : m ≤ m𝓧
hμν : μ ≪ ν
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ Integrable (fun x ↦ ((∂μ.trim hm/∂ν.trim hm) x).toReal) (ν.trim hm)

Tactic:
fun_prop

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

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
h_int : Integrable (llr μ ν) μ
⊢ StronglyMeasurable klFun

Tactic:
fun_prop

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

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
h_int : Integrable (llr μ ν) μ
⊢ ContinuousWithinAt klFun (Ici 0) 0

Tactic:
fun_prop

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

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
⊢ StronglyMeasurable fun x ↦ klFun ((∂Measure.map g μ/∂Measure.map g ν) x).toReal

Tactic:
fun_prop

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
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
mE : MeasurableSpace E
inst✝¹ : BorelSpace E
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hφ_meas : StronglyMeasurable φ
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
⊢ StronglyMeasurable (φ ∘ μ[f | m])

Tactic:
fun_prop

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
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
mE : MeasurableSpace E
inst✝¹ : BorelSpace E
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hφ_meas : StronglyMeasurable φ
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
⊢ StronglyMeasurable μ[φ ∘ f | m]

Tactic:
fun_prop

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
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
mE : MeasurableSpace E
inst✝¹ : BorelSpace E
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ s φ
hφ_cont : UpperSemicontinuousOn φ s
hφ_meas : StronglyMeasurable φ
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
⊢ StronglyMeasurable μ[φ ∘ f | m]

Tactic:
fun_prop

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
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
mE : MeasurableSpace E
inst✝¹ : BorelSpace E
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ s φ
hφ_cont : UpperSemicontinuousOn φ s
hφ_meas : StronglyMeasurable φ
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
⊢ StronglyMeasurable (φ ∘ μ[f | m])

Tactic:
fun_prop

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
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
mE : MeasurableSpace E
inst✝¹ : BorelSpace E
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConvexOn ℝ univ φ
hφ_cont : LowerSemicontinuous φ
hφ_meas : StronglyMeasurable φ
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
⊢ StronglyMeasurable (φ ∘ μ[f | m])

Tactic:
fun_prop

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
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
mE : MeasurableSpace E
inst✝¹ : BorelSpace E
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConvexOn ℝ univ φ
hφ_cont : LowerSemicontinuous φ
hφ_meas : StronglyMeasurable φ
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
⊢ StronglyMeasurable μ[φ ∘ f | m]

Tactic:
fun_prop

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

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hg : Measurable g
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ StronglyMeasurable klFun

Tactic:
fun_prop

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

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hg : Measurable g
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hf : StronglyMeasurable klFun
⊢ ContinuousWithinAt klFun (Ici 0) 0

Tactic:
fun_prop

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
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
mE : MeasurableSpace E
inst✝¹ : BorelSpace E
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ univ φ
hφ_cont : UpperSemicontinuous φ
hφ_meas : StronglyMeasurable φ
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
⊢ StronglyMeasurable μ[φ ∘ f | m]

Tactic:
fun_prop

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
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
mE : MeasurableSpace E
inst✝¹ : BorelSpace E
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ univ φ
hφ_cont : UpperSemicontinuous φ
hφ_meas : StronglyMeasurable φ
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
⊢ StronglyMeasurable (φ ∘ μ[f | m])

Tactic:
fun_prop

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : Ring k
inst✝⁶ : PartialOrder k
inst✝⁵ : IsOrderedAddMonoid k
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Module k V
n : ℕ
inst✝¹ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
inst✝ : ZeroLEOneClass k
p : P
x✝ : p ∈ s.closedInterior ∩ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) 0)
hp : p ∈ s.closedInterior
hshift : p ∈ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) 0)
⊢ p ∈ {s.points i}

Tactic:
obtain ⟨w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype <|
    s.closedInterior_subset_affineSpan hp

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : Ring k
inst✝⁶ : PartialOrder k
inst✝⁵ : IsOrderedAddMonoid k
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Module k V
n : ℕ
inst✝¹ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
inst✝ : ZeroLEOneClass k
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
x✝ :
  (affineCombination k univ s.points) w ∈ s.closedInterior ∩ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) 0)
hp : (affineCombination k univ s.points) w ∈ s.closedInterior
hshift : (affineCombination k univ s.points) w ∈ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) 0)
⊢ (affineCombination k univ s.points) w ∈ {s.points i}
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
P : Type u_5
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : Module S P
inst✝ : IsScalarTower R S P
α : M →ₗ[R] P
j : IsBaseChange S α
f : M →ₗ[R] M
⊢ ↑R (j.endHom f) ∘ₗ α = α ∘ₗ f

Tactic:
by
  ext; simp [endHom_comp_apply]

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
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
i : ι
⊢ f (b i) = (b.coord i) (f (b i)) • b i

Tactic:
rw [b.ext_elem_iff]

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
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
i : ι
⊢ ∀ (i_1 : ι), (b.repr (f (b i))) i_1 = (b.repr ((b.coord i) (f (b i)) • b i)) i_1
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f : Dual R V
v : V
r s : R
x : V
⊢ (transvection f (r • v) ∘ₗ transvection f (s • v)) x = (transvection f ((r + s + s * f v * r) • v)) x

Tactic:
simp only [LinearMap.comp_apply, apply, map_add, map_smul, add_assoc]

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f : Dual R V
v : V
r s : R
x : V
⊢ x + (f x • r • v + f x • s • (v + f v • r • v)) = x + f x • (r + (s + s * f v * r)) • v
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 + t * (r * (b.repr (f (b j))) j) = 0
⊢ s * r + t * r * (b.coord j) (f (b j)) = 0

Tactic:
add_right_comm,

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)) = 0
this : s * r + t * (r * (b.repr (f (b j))) j) + t * (b.repr (f (b i))) j = 0
⊢ s * r + t * r * (b.coord j) (f (b j)) = 0
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
h : IsUnit (1 + f v)
x : V
⊢ f x * ↑(-h.unit⁻¹) + (f x * 1 + f x * ↑(-h.unit⁻¹) * f v) = 0

Tactic:
rw [mul_assoc, ← mul_add, ← mul_add]

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
h : IsUnit (1 + f v)
x : V
⊢ f x * (↑(-h.unit⁻¹) + (1 + ↑(-h.unit⁻¹) * f v)) = 0
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
⊢ (ofBaseChange A Q).comp (toBaseChange A Q) = AlgHom.id A (CliffordAlgebra (QuadraticForm.baseChange A Q))

Tactic:
by
  ext x
  change ofBaseChange A Q (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] x)))
    = ι (Q.baseChange A) (1 ⊗ₜ[R] x)
  rw [toBaseChange_ι, ofBaseChange_tmul_ι]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (algebraMap R (CliffordAlgebra (Q' Q))) (QuadraticMap.polar ⇑(Q' Q) (0, 1) ((LinearMap.inl R M R) m)) = 0

Tactic:
simp [QuadraticMap.polar]

Goal state after: