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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κs : ι → Kernel α β
I : Finset ι
h : ∀ i ∈ I, IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel (∑ i ∈ I, κs i)

Tactic:
induction I using Finset.induction with
  | empty => rw [Finset.sum_empty]; infer_instance
  | insert i I hi_notMem_I h_ind =>
    rw [Finset.sum_insert hi_notMem_I]
    have : IsSFiniteKernel (κs i) := h i (Finset.mem_insert_self _ _)
    have : IsSFiniteKernel (∑ x ∈ I, κs x) :=
      h_ind fun i hiI => h i (Finset.mem_insert_of_mem hiI)
    exact IsSFiniteKernel.add _ _

Goal state after:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: case left
α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), ↑c ≠ []
⊢ r ≤ ∑ i, (↑(w i)).length

Tactic:
have : ∑ _, 1 ≤ ∑ i, (w i).val.length :=
      Finset.sum_le_sum (fun i _ => by grind)
    simpa using this

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h : ¬IsSFiniteKernel κ
⊢ μ ⊗ₘ κ = 0

Tactic:
rw [compProd, Kernel.compProd_of_not_isSFiniteKernel_right, zero_apply]

Goal state after:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h : ¬IsSFiniteKernel κ
⊢ ¬IsSFiniteKernel (Kernel.prodMkLeft Unit κ)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hf : Measurable f
hg : ¬Measurable g
this : ¬Measurable fun x ↦ (f x, g x)
⊢ (κ.map fun x ↦ (f x, g x)).snd = κ.map g

Tactic:
simp [map_of_not_measurable _ hg, map_of_not_measurable _ this]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: case pos.e_f
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
d : T
⊢ ∫⁻ (x : Y), (Measure.dirac (x, d).swap) s ∂κ ac.1 = (κ ac.1) (Prod.mk d ⁻¹' s)

Tactic:
simp_rw [Prod.swap_prod_mk, Measure.dirac_apply' _ hs, ← Set.indicator_comp_right,
    lintegral_indicator (measurable_prodMk_left hs)]

Goal state after:
case pos.e_f
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
d : T
⊢ ∫⁻ (a : Y) in Prod.mk d ⁻¹' s, (1 ∘ Prod.mk d) a ∂κ ac.1 = (κ ac.1) (Prod.mk d ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔ ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η

Tactic:
rw [(withDensity_absolutelyContinuous ν (μ.rnDeriv ν)).mutuallySingular_compProd_iff]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η ↔
    ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
Module: Mathlib.Probability.Kernel.Composition.RadonNikodym

Goal state before:
pp: case refine_4
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
x✝ : (ν ⊗ₘ κ) s < ∞
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
f' : ℕ → Set (α × β)
hf_disj : Pairwise (Function.onFun Disjoint f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (x : α × β) in f' i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in f' i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∑' (i : ℕ), ∫⁻ (a : α × β) in f' i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) a ∂ν ⊗ₘ κ =
    ∫⁻ (x : α × β) in ⋃ i, f' i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

Tactic:
lintegral_iUnion hf_meas hf_disj

Goal state after:
case refine_4
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
x✝ : (ν ⊗ₘ κ) s < ∞
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
f' : ℕ → Set (α × β)
hf_disj : Pairwise (Function.onFun Disjoint f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (x : α × β) in f' i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in f' i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∑' (i : ℕ), ∫⁻ (a : α × β) in f' i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) a ∂ν ⊗ₘ κ =
    ∑' (i : ℕ), ∫⁻ (a : α × β) in f' i, μ.rnDeriv ν a.1 ∂ν ⊗ₘ κ
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case neg.e_a
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : ¬μ Set.univ = ∞
⊢ ENNReal.ofReal ((μ.real Set.univ)⁻¹ * 1) = (μ Set.univ)⁻¹

Tactic:
mul_one,

Goal state after:
case neg.e_a
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : ¬μ Set.univ = ∞
⊢ ENNReal.ofReal (μ.real Set.univ)⁻¹ = (μ Set.univ)⁻¹
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ klDiv μ ν = if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞

Tactic:
klDiv_eq_integral_klFun

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c
⊢ Integrable (llr (c • μ) ν) (c • μ)

pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c
⊢ ∫ (a : α), llr (c • μ) ν a ∂c • μ + ν.real univ - (c • μ).real univ =
    ↑c * (∫ (a : α), llr μ ν a ∂μ + ν.real univ - μ.real univ) + (1 - ↑c) * ν.real univ + ↑c * log ↑c * μ.real univ

Tactic:
· refine Integrable.smul_measure_nnreal ?_
    rw [integrable_congr h_llr]
    fun_prop

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c
⊢ ∫ (a : α), llr (c • μ) ν a ∂c • μ + ν.real univ - (c • μ).real univ =
    ↑c * (∫ (a : α), llr μ ν a ∂μ + ν.real univ - μ.real univ) + (1 - ↑c) * ν.real univ + ↑c * log ↑c * μ.real univ
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 : ℕ
⊢ ∀ᵐ (a : α) ∂μ, ↑↑(m (u n)) a = ↑↑f a • u n

Tactic:
filter_upwards [(toSpanSingleton ℝ (u n)).coeFn_compLp f] with x hx using by simp [m, hx]

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 μ ν) μ
c : ℝ≥0
hc : c = 0
⊢ (klDiv (c • μ) (c • ν)).toReal = ↑c * (klDiv μ ν).toReal

pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
⊢ (klDiv (c • μ) (c • ν)).toReal = ↑c * (klDiv μ ν).toReal

Tactic:
· simp [hc]

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

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : c = 0
⊢ klDiv (c • μ) (c • ν) = ↑c * klDiv μ ν

pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : ¬c = 0
⊢ klDiv (c • μ) (c • ν) = ↑c * klDiv μ ν

Tactic:
· simp [hc]

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : ¬c = 0
⊢ klDiv (c • μ) (c • ν) = ↑c * klDiv μ ν
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : ν.real univ * (μ.real univ / ν.real univ) = μ.real univ
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ)) + ν.real univ * 1 -
      ν.real univ * (μ.real univ / ν.real univ)

Tactic:
mul_one,

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᵐ[μ.restrict s] 0
h_nnnorm_eq_zero : (fun x ↦ ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊) =ᵐ[μ.restrict s] 0
⊢ ↑↑↑((condExpL2 ℝ ℝ hm) f) =ᵐ[μ.restrict s] 0

Tactic:
refine h_nnnorm_eq_zero.mono fun x hx => ?_
      dsimp only at hx
      rw [Pi.zero_apply] at hx ⊢
      · rwa [ENNReal.coe_eq_zero, nnnorm_eq_zero] at hx

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

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
hY : AEMeasurable Y (P.trim hm)
hXY : ∀ (s : Set Ω), MeasurableSet s → ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
⊢ Y =ᵐ[P] P⁻[X | mΩ]

Tactic:
by
  apply ae_eq_of_ae_eq_trim
  apply ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ hY (by fun_prop)
  intro s hs _
  rw [setLIntegral_trim_ae hm hY hs, setLIntegral_condLExp_trim _ _ _ hs]
  exact hXY s hs

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

Goal state before:
pp: case refine_1
𝓧 : 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 < ∞ → IntegrableOn (fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) (g a)).toReal) s ν

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 ∂ν

pp: case refine_3
𝓧 : 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 ν
⊢ AEStronglyMeasurable (fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) (g a)).toReal) ν

Tactic:
· rintro _ ⟨t, _, rfl⟩ _
    exact Integrable.integrableOn (Measure.integrable_toReal_rnDeriv.comp_measurable hg)

Goal state after:
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 ∂ν

case refine_3
𝓧 : 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 ν
⊢ AEStronglyMeasurable (fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) (g a)).toReal) ν
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 (ν.trim ⋯)
this : SigmaFinite ν
t : Set 𝓨
ht : MeasurableSet t
a✝ : ν (g ⁻¹' t) < ∞
⊢ ∫ (y : 𝓨) in t, ((Measure.map g μ).rnDeriv (Measure.map g ν) y).toReal ∂Measure.map g ν =
    ∫ (x : 𝓧) in g ⁻¹' t, (μ.rnDeriv ν x).toReal ∂ν

Tactic:
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.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) ν
h : Integrable (fun x ↦ f ((∂μ.trim hm/∂ν.trim hm) x).toReal) (ν.trim hm)
⊢ (fun x ↦ f ((∂μ.trim hm/∂ν.trim hm) x).toReal) =ᵐ[ν.trim hm] fun x ↦ f (ν[fun x ↦ ((∂μ/∂ν) x).toReal | m] x)

Tactic:
filter_upwards [toReal_rnDeriv_trim hm hμν] with a ha

Goal state after:
𝓧 : 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) ν
h : Integrable (fun x ↦ f ((∂μ.trim hm/∂ν.trim hm) x).toReal) (ν.trim hm)
a : 𝓧
ha : ((∂μ.trim hm/∂ν.trim hm) a).toReal = ν[fun x ↦ ((∂μ/∂ν) x).toReal | m] a
⊢ f ((∂μ.trim hm/∂ν.trim hm) a).toReal = f (ν[fun x ↦ ((∂μ/∂ν) x).toReal | m] a)
Module: Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Goal state before:
pp: case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hg : Measurable g
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ENNReal.ofReal (∫ (x : 𝓧), klFun (ν[fun x ↦ ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] x) ∂ν) ≤ klDiv μ ν

Tactic:
klDiv_eq_integral_klFun

Goal state after:
case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hg : Measurable g
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ENNReal.ofReal (∫ (x : 𝓧), klFun (ν[fun x ↦ ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] x) ∂ν) ≤
    if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : 𝓧), klFun ((∂μ/∂ν) x).toReal ∂ν) else ∞
Module: Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Goal state before:
pp: case h
𝓧 : 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
hf_cont : ContinuousWithinAt klFun (Ici 0) 0
⊢ ∫ (x : 𝓧), klFun (ν[fun x ↦ ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] x) ∂ν ≤
    ∫ (x : 𝓧), ν[fun x ↦ klFun ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] x ∂ν

Tactic:
have h_int' : Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν := by
    rwa [integrable_klFun_rnDeriv_iff hμν]

Goal state after:
case h
𝓧 : 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
hf_cont : ContinuousWithinAt klFun (Ici 0) 0
h_int' : Integrable (fun x ↦ klFun ((∂μ/∂ν) x).toReal) ν
⊢ ∫ (x : 𝓧), klFun (ν[fun x ↦ ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] x) ∂ν ≤
    ∫ (x : 𝓧), ν[fun x ↦ klFun ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] x ∂ν
Module: Mathlib.LinearAlgebra.AffineSpace.Matrix

Goal state before:
pp: ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (b.toMatrix ⇑b₂).det
⊢ b.coords x ᵥ* (b.toMatrix ⇑b₂)⁻¹ = b₂.coords x

Tactic:
rw [← b.toMatrix_vecMul_coords b₂, Matrix.vecMul_vecMul, Matrix.mul_nonsing_inv _ hu,
    Matrix.vecMul_one]

Goal state after:
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 ε
v : V
i : ι
| ((basis b ibc).repr (ε ((b.repr v).sum fun i a ↦ a • b i))) i

Tactic:
map_finsuppSum,

Goal state after:
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 ε
v : V
i : ι
| ((basis b ibc).repr ((b.repr v).sum fun a b_1 ↦ ε (b_1 • b a))) i
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₂
⊢ ↑(alternatization (a.domCoprod b)) = ↑((alternatization a).domCoprod (alternatization b))

Tactic:
domCoprod_coe,

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₂
⊢ ↑(alternatization (a.domCoprod b)) = ∑ σ, domCoprod.summand (alternatization a) (alternatization b) σ
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
this : s + t * (b.repr (f (b i))) i + t * r * (b.repr (f (b j))) i = 0
⊢ s + t * (b.coord i) (f (b i)) = 0

Tactic:
add_eq_zero_iff_eq_neg

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

Tactic:
add_eq_zero_iff_eq_neg

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 : s * r + t * r * (b.coord j) (f (b j)) = 0
⊢ (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))