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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
hf : Measurable f
a : α
⊢ (κ a) (f ⁻¹' Set.univ) = 1

Tactic:
Set.preimage_univ,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
hf : Measurable f
a : α
⊢ (κ a) Set.univ = 1
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
f : β → γ
hf : Measurable f
⊢ (κ.map fun a ↦ (a, f a)).fst = κ

Tactic:
fst_map_prod _ hf,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
f : β → γ
hf : Measurable f
⊢ (κ.map fun a ↦ a) = κ
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 ν
⊢ (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔
    ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η

Tactic:
rw [compProd_add_left, MutuallySingular.add_left_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : β → Prop
hp : MeasurableSet {z | p z}
h : ∀ᵐ (y : α) ∂μ, ∀ᵐ (z : β) ∂κ y, p z
⊢ ∀ᵐ (z : β) ∂⇑κ ∘ₘ μ, p z

Tactic:
by
  rw [comp_eq_comp_const_apply]
  exact Kernel.ae_comp_of_ae_ae hp h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦
    ∫ (x : β), ∫ (y : γ), ↑↑f (x, y) ∂η (a, x) ∂κ a

Tactic:
rw [continuous_iff_continuousAt]; intro g
  refine
    tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_compProd.aestronglyMeasurable
      (Eventually.of_forall fun h => (L1.integrable_coeFn h).integral_compProd) ?_
  simp_rw [← lintegral_fn_integral_sub (‖·‖ₑ) (L1.integrable_coeFn _) (L1.integrable_coeFn g)]
  apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds _ (fun i => zero_le) _
  · exact fun i => ∫⁻ x, ∫⁻ y, ‖i (x, y) - g (x, y)‖ₑ ∂η (a, x) ∂κ a
  swap; · exact fun i => lintegral_mono fun x => enorm_integral_le_lintegral_enorm _
  have (i : Lp (α := β × γ) E 1 (((κ ⊗ₖ η) a) : Measure (β × γ))) :
      Measurable fun z => ‖i z - g z‖ₑ :=
    ((Lp.stronglyMeasurable i).sub (Lp.stronglyMeasurable g)).enorm
  simp_rw [← lintegral_compProd _ _ _ (this _), ← L1.ofReal_norm_sub_eq_lintegral, ← ofReal_zero]
  refine (continuous_ofReal.tendsto 0).comp ?_
  rw [← tendsto_iff_norm_sub_tendsto_zero]
  exact tendsto_id

Goal state after:
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 (α × β)),
    Pairwise (Function.onFun Disjoint f) →
      (∀ (i : ℕ), MeasurableSet (f i)) →
        (∀ (i : ℕ),
            ∫⁻ (x : α × β) in f i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
              ∫⁻ (x : α × β) in f i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ) →
          ∫⁻ (x : α × β) in ⋃ i, f i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
            ∫⁻ (x : α × β) in ⋃ i, f i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

Tactic:
· intro f' hf_disj hf_meas hf_eq
    rw [lintegral_iUnion hf_meas hf_disj, lintegral_iUnion hf_meas hf_disj]
    congr with i
    exact hf_eq i

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

Goal state before:
pp: case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h : μ = 0
⊢ (μ.tilted fun x ↦ c) = (μ Set.univ)⁻¹ • μ

Tactic:
rw [h]

Goal state after:
case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h : μ = 0
⊢ (Measure.tilted 0 fun x ↦ c) = (0 Set.univ)⁻¹ • 0
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (z : β × γ) in s ×ˢ Set.univ, f z ∂(κ ⊗ₖ η) a = ∫⁻ (x : β) in s, ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a

Tactic:
setLIntegral_compProd κ η a hf hs MeasurableSet.univ,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (x : β) in s, ∫⁻ (y : γ) in Set.univ, f (x, y) ∂η (a, x) ∂κ a =
    ∫⁻ (x : β) in s, ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
η : Kernel (α × β) γ
⊢ κ ⊗ₖ η = Kernel.sum fun n ↦ κ.seq n ⊗ₖ η

Tactic:
compProd_def

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
η : Kernel (α × β) γ
⊢ swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    Kernel.sum fun n ↦
      swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β) ∘ₖ
          (Kernel.id ∥ₖ κ.seq n) ∘ₖ
        copy α
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
⊢ κ ⊗ₖ η = Kernel.sum fun n ↦ κ ⊗ₖ η.seq n

Tactic:
compProd_def

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
⊢ swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    Kernel.sum fun n ↦
      swap γ β ∘ₖ (η.seq n ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β) ∘ₖ
          (Kernel.id ∥ₖ κ) ∘ₖ
        copy α
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsZeroOrMarkovKernel κ
η : Kernel (α × β) γ
inst✝ : IsZeroOrMarkovKernel η
⊢ IsZeroOrMarkovKernel (κ ⊗ₖ η)

Tactic:
compProd_def

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsZeroOrMarkovKernel κ
η : Kernel (α × β) γ
inst✝ : IsZeroOrMarkovKernel η
⊢ IsZeroOrMarkovKernel
    (swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α)
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsFiniteKernel η
⊢ IsFiniteKernel (κ ⊗ₖ η)

Tactic:
compProd_def

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsFiniteKernel η
⊢ IsFiniteKernel
    (swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α)
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
η : Kernel (α × β) γ
⊢ IsSFiniteKernel (κ ⊗ₖ η)

Tactic:
compProd_def

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
η : Kernel (α × β) γ
⊢ IsSFiniteKernel
    (swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α)
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f : β × γ → E
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ((κ ⊗ₖ η) a)
⊢ Integrable f ((κ.restrict hs ⊗ₖ η.restrict ht) a)

Tactic:
· rw [compProd_restrict, Kernel.restrict_apply]; exact hf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
f : γ → E
hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)
⊢ HasFiniteIntegral f ((η ∘ₖ κ) a) ↔
    (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral f (η x)) ∧ HasFiniteIntegral (fun x ↦ ∫ (y : γ), ‖f y‖ ∂η x) (κ a)

Tactic:
by
  rw [hasFiniteIntegral_congr hf.ae_eq_mk, hasFiniteIntegral_comp_iff hf.stronglyMeasurable_mk]
  refine and_congr (eventually_congr ?_) (hasFiniteIntegral_congr ?_)
  · filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk.symm] with _ hx using
      hasFiniteIntegral_congr hx
  · filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk.symm] with _ hx using
      integral_congr_ae (EventuallyEq.fun_comp hx _)

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

Goal state before:
pp: case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h : μ = 0
⊢ ∫ (x : α), rexp (g x) ∂μ.tilted f = (∫ (x : α), rexp ((f + g) x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
rw [h]

Goal state after:
case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h : μ = 0
⊢ ∫ (x : α), rexp (g x) ∂Measure.tilted 0 f = (∫ (x : α), rexp ((f + g) x) ∂0) / ∫ (x : α), rexp (f x) ∂0
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ Integrable (llr (μ.tilted f) ν) μ

Tactic:
integrable_congr (llr_tilted_left hμν hfμ hfν)

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ Integrable (fun x ↦ f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x) μ
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: case hf
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun a ↦ (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal) ν

Tactic:
rwa [integrable_rnDeriv_mul_log_iff hμν]

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

Goal state before:
pp: case hf
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun x ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal) ν

Tactic:
rwa [integrable_rnDeriv_mul_log_iff hμν]

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

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x y : G
⊢ condExpIndL1 hm μ s (x + y) = condExpIndL1 hm μ s x + condExpIndL1 hm μ s y

Tactic:
by
  by_cases hs : MeasurableSet s
  swap; · simp_rw [condExpIndL1_of_not_measurableSet hs]; rw [zero_add]
  by_cases hμs : μ s = ∞
  · simp_rw [condExpIndL1_of_measure_eq_top hμs]; rw [zero_add]
  · simp_rw [condExpIndL1_of_measurableSet_of_measure_ne_top hs hμs]
    exact condExpIndL1Fin_add hs hμs x y

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hp : 1 ≤ ∞
h'f : ∑' (n : ι), eLpNorm (f n) ∞ μ ≠ ∞
this : ∀ᵐ (x : X) ∂μ, ∀ (n : ι), ‖f n x‖ₑ ≤ eLpNorm (f n) ∞ μ
x : X
hx : ∀ (n : ι), ‖f n x‖ₑ ≤ eLpNorm (f n) ∞ μ
⊢ ∑' (n : ι), ‖f n x‖ₑ ≤ ∑' (n : ι), eLpNorm (f n) ∞ μ

Tactic:
gcongr with i

Goal state after:
case h
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hp : 1 ≤ ∞
h'f : ∑' (n : ι), eLpNorm (f n) ∞ μ ≠ ∞
this : ∀ᵐ (x : X) ∂μ, ∀ (n : ι), ‖f n x‖ₑ ≤ eLpNorm (f n) ∞ μ
x : X
hx : ∀ (n : ι), ‖f n x‖ₑ ≤ eLpNorm (f n) ∞ μ
i : ι
⊢ ‖f i x‖ₑ ≤ eLpNorm (f i) ∞ μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: case neg
α : Type u_1
F : Type u_2
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝² : SigmaFinite (μ.trim hm)
inst✝¹ : NormedSpace ℝ F
inst✝ : SMulCommClass ℝ 𝕜 F
c : 𝕜
x : F
hs : MeasurableSet s
hμs : ¬μ s = ∞
⊢ condExpIndL1 hm μ s (c • x) = c • condExpIndL1 hm μ s x

Tactic:
simp_rw [condExpIndL1_of_measurableSet_of_measure_ne_top hs hμs]
    exact condExpIndL1Fin_smul' hs hμs c x

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
s : Set X
hs : MeasurableSet s
h's : μ s ≠ ∞
this : ∑' (n : ι), eLpNorm (f n) p (μ.restrict s) * (μ.restrict s) Set.univ ^ (1 / ENNReal.toReal 1 - 1 / p.toReal) < ∞
⊢ ∑' (i : ι), ∫⁻ (a : X) in s, ‖f i a‖ₑ ∂μ ≤
    ∑' (n : ι), eLpNorm (f n) p (μ.restrict s) * (μ.restrict s) Set.univ ^ (1 / ENNReal.toReal 1 - 1 / p.toReal)

Tactic:
gcongr with i

Goal state after:
case h
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
s : Set X
hs : MeasurableSet s
h's : μ s ≠ ∞
this : ∑' (n : ι), eLpNorm (f n) p (μ.restrict s) * (μ.restrict s) Set.univ ^ (1 / ENNReal.toReal 1 - 1 / p.toReal) < ∞
i : ι
⊢ ∫⁻ (a : X) in s, ‖f i a‖ₑ ∂μ ≤
    eLpNorm (f i) p (μ.restrict s) * (μ.restrict s) Set.univ ^ (1 / ENNReal.toReal 1 - 1 / p.toReal)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
G : Type u_4
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 ≠ ∞
c : G
⊢ (condExpInd G hm μ s) c = indicatorConstLp 1 ⋯ hμs c

Tactic:
by
  ext1
  grw [indicatorConstLp_coeFn, condExpInd_ae_eq_condExpIndSMul hm (hm s hs) hμs,
    condExpIndSMul_ae_eq_smul]
  rw [condExpL2_indicator_of_measurable hm hs hμs (1 : ℝ)]
  filter_upwards [@indicatorConstLp_coeFn α _ _ 2 μ _ s (hm s hs) hμs (1 : ℝ)] with x hx
  rw [hx]
  by_cases hx_mem : x ∈ s <;> simp [hx_mem]

Goal state after:
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
hm_not : ¬m ≤ m₀
⊢ μ[f | m] = 0

Tactic:
by rw [condExp, dif_neg hm_not]

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

pp: case pos
α : 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]; rfl

Goal state after:
case pos
α : 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]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: case refine_2
α : 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 : ↥(Lp F' 1 μ)
⊢ ∀ ⦃f g : α → F'⦄ (hf : MemLp f 1 μ) (hg : MemLp g 1 μ),
    Disjoint (Function.support f) (Function.support g) →
      AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf))) μ →
        AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg))) μ →
          AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf + MemLp.toLp g hg))) μ

Tactic:
intro f g hf hg _ hfm hgm

Goal state after:
case refine_2
α : 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✝ : ↥(Lp F' 1 μ)
f g : α → F'
hf : MemLp f 1 μ
hg : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hfm : AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf))) μ
hgm : AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg))) μ
⊢ AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf + MemLp.toLp g hg))) μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: α : Type u_1
G' : Type u_6
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace ℝ G'
inst✝ : CompleteSpace G'
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
x : G'
⊢ (∫ (a : α) in s, ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 ht hμt 1)) a ∂μ) • x = μ.real (t ∩ s) • x

Tactic:
setIntegral_condExpL2_indicator hs ht hμs hμt

Goal state after:
α : Type u_1
G' : Type u_6
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace ℝ G'
inst✝ : CompleteSpace G'
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
x : G'
⊢ μ.real (t ∩ s) • x = μ.real (t ∩ s) • x
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
inst✝ : SigmaFinite (μ.trim hm)
h : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      (μ.trim hm) s_1 < ∞ →
        0 ≤
          ∫ (x : α) in s_1,
            AEStronglyMeasurable.mk (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h x ∂μ.trim hm

Tactic:
· intro t ht hμt
    rw [← setIntegral_trim hm h.stronglyMeasurable_mk ht]
    have h_ae :
        ∀ᵐ x ∂μ, x ∈ t → h.mk _ x = (condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1) : α → ℝ) x := by
      filter_upwards [h.ae_eq_mk] with x hx using fun _ => hx.symm
    rw [setIntegral_congr_ae (hm t ht) h_ae,
      setIntegral_condExpL2_indicator ht hs ((le_trim hm).trans_lt hμt).ne hμs]
    exact ENNReal.toReal_nonneg

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

pp: case pos
α : 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]; rfl

Goal state after:
case pos
α : 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
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : 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)
A : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), μ[f i | m] a = ↑↑(condExpL1 hm μ (f i)) a
⊢ ∑' (n : ι), ‖condExpL1 hm μ (f n)‖ₑ ≤ ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ

Tactic:
gcongr with i

Goal state after:
case h
α : 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)
A : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), μ[f i | m] a = ↑↑(condExpL1 hm μ (f i)) a
i : ι
⊢ ‖condExpL1 hm μ (f i)‖ₑ ≤ ∫⁻ (a : α), ‖f i a‖ₑ ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hm : ¬mΩ ≤ mΩ₀
⊢ Measurable P⁻[X | mΩ]

Tactic:
· simp [condLExp_of_not_le hm, measurable_zero]

Goal state after: