awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : NormedSpace ℝ γ
inst_5 : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
A : AEStronglyMeasurable (m₀ := inst_2) id (Measure.map f μ)
pos : Eq (α := γ) (@integral _ _ _ _ inst_2 (Measure.map f μ) fun (y : γ) ↦ id y) (∫ (x : β), id (g x) ∂ν)
⊢ Eq.{u_3 + 1} (α := γ) (∫ (x : α), id (f x) ∂μ) (∫ (x : β), id (g x) ∂ν)

Tactic:
rw [← integral_map h.aemeasurable_fst A]

Premises used: MeasureTheory.integral_map, ProbabilityTheory.IdentDistrib.aemeasurable_fst
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : NormedSpace ℝ γ
inst_5 : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
A : AEStronglyMeasurable (m₀ := inst_2) id (Measure.map f μ)
⊢ AEStronglyMeasurable (m₀ := inst_2) id (Measure.map g ν)

Tactic:
rw [h.map_eq] at A

Premises used: ProbabilityTheory.IdentDistrib.map_eq
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : NormedSpace ℝ γ
inst_5 : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
A : AEStronglyMeasurable (m₀ := inst_2) id (Measure.map g ν)
pos :
  Eq (α := γ) (@integral _ _ _ _ inst_2 (Measure.map f μ) fun (y : γ) ↦ id y)
    (@integral _ _ _ _ inst_2 (Measure.map g ν) fun (y : γ) ↦ id y)
pos₁ pos₂ :
  Eq (α := γ) (@integral _ _ _ _ inst_2 (Measure.map g ν) fun (y : γ) ↦ id y)
    (@integral _ _ _ _ inst_2 (Measure.map g ν) fun (y : γ) ↦ id y)
⊢ Eq (α := γ) (@integral _ _ _ _ inst_2 (Measure.map f μ) fun (y : γ) ↦ id y) (∫ (x : β), id (g x) ∂ν)

Tactic:
rw [← integral_map h.aemeasurable_snd A, h.map_eq]

Premises used: MeasureTheory.integral_map, ProbabilityTheory.IdentDistrib.aemeasurable_snd, ProbabilityTheory.IdentDistrib.map_eq
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : NormedSpace ℝ γ
inst_5 : BorelSpace γ
h : IdentDistrib f g μ ν
hf : ¬AEStronglyMeasurable f μ
neg : Eq.{u_3 + 1} (α := γ) 0 (∫ (x : β), g x ∂ν)
⊢ Eq.{u_3 + 1} (α := γ) (∫ (x : α), f x ∂μ) (∫ (x : β), g x ∂ν)

Tactic:
rw [integral_non_aestronglyMeasurable hf]

Premises used: MeasureTheory.integral_non_aestronglyMeasurable
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : NormedSpace ℝ γ
inst_5 : BorelSpace γ
h : IdentDistrib f g μ ν
hf : ¬AEStronglyMeasurable f μ
⊢ ¬AEStronglyMeasurable g ν

Tactic:
rw [h.aestronglyMeasurable_iff] at hf

Premises used: ProbabilityTheory.IdentDistrib.aestronglyMeasurable_iff
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : NormedSpace ℝ γ
inst_5 : BorelSpace γ
h : IdentDistrib f g μ ν
hf : ¬AEStronglyMeasurable g ν
neg neg₁ : Eq.{u_3 + 1} (α := γ) 0 0
⊢ Eq.{u_3 + 1} (α := γ) 0 (∫ (x : β), g x ∂ν)

Tactic:
rw [integral_non_aestronglyMeasurable hf]

Premises used: MeasureTheory.integral_non_aestronglyMeasurable
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
pos : ∀ (h0 : p = 0), eLpNorm f p μ = eLpNorm g p ν
neg : ∀ (h0 : ¬p = 0), eLpNorm f p μ = eLpNorm g p ν
⊢ eLpNorm f p μ = eLpNorm g p ν

Tactic:
by_cases h0 : p = 0
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : p = 0
⊢ eLpNorm f p μ = eLpNorm g p ν

Tactic:
simp [h0]
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
pos : ∀ (h_top : p = ∞), eLpNorm f p μ = eLpNorm g p ν
neg : ∀ (h_top : ¬p = ∞), eLpNorm f p μ = eLpNorm g p ν
⊢ eLpNorm f p μ = eLpNorm g p ν

Tactic:
by_cases h_top : p = ∞
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ∞
pos : Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) (essSup (fun (x : β) ↦ ‖g x‖ₑ) ν)
⊢ eLpNorm f p μ = eLpNorm g p ν

Tactic:
simp only [h_top, eLpNorm, eLpNormEssSup, ENNReal.top_ne_zero, if_true,
      if_false]

Premises used: if_true, if_false, MeasureTheory.eLpNormEssSup, ENNReal.top_ne_zero, MeasureTheory.eLpNorm
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ∞
pos : IdentDistrib (γ := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : β) ↦ ‖g x‖ₑ) μ ν
⊢ Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) (essSup (fun (x : β) ↦ ‖g x‖ₑ) ν)

Tactic:
apply essSup_eq

Premises used: ProbabilityTheory.IdentDistrib.essSup_eq
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ∞
⊢ IdentDistrib (γ := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : β) ↦ ‖g x‖ₑ) μ ν

Tactic:
h.comp (measurable_coe_nnreal_ennreal.comp measurable_nnnorm)

Premises used: Measurable.comp, ProbabilityTheory.IdentDistrib.comp, measurable_coe_nnreal_ennreal, measurable_nnnorm
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ∞
⊢ IdentDistrib (γ := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : β) ↦ ‖g x‖ₑ) μ ν

Tactic:
exact h.comp (measurable_coe_nnreal_ennreal.comp measurable_nnnorm)

Premises used: Measurable.comp, ProbabilityTheory.IdentDistrib.comp, measurable_coe_nnreal_ennreal, measurable_nnnorm
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ∞
neg : (∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ = (∫⁻ (a : β), ‖g a‖ₑ ^ p.toReal ∂ν) ^ p.toReal⁻¹
⊢ eLpNorm f p μ = eLpNorm g p ν

Tactic:
simp only [eLpNorm_eq_eLpNorm' h0 h_top, eLpNorm', one_div]

Premises used: MeasureTheory.eLpNorm', MeasureTheory.eLpNorm_eq_eLpNorm', one_div
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ∞
neg : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ = ∫⁻ (a : β), ‖g a‖ₑ ^ p.toReal ∂ν
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ = (∫⁻ (a : β), ‖g a‖ₑ ^ p.toReal ∂ν) ^ p.toReal⁻¹

Tactic:
congr 1
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ∞
neg : IdentDistrib (γ := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) (fun (x : β) ↦ ‖g x‖ₑ ^ p.toReal) μ ν
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ = ∫⁻ (a : β), ‖g a‖ₑ ^ p.toReal ∂ν

Tactic:
apply lintegral_eq

Premises used: ProbabilityTheory.IdentDistrib.lintegral_eq
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ IdentDistrib (γ := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) (fun (x : β) ↦ ‖g x‖ₑ ^ p.toReal) μ ν

Tactic:
h.comp (Measurable.pow_const (measurable_coe_nnreal_ennreal.comp measurable_nnnorm)
    p.toReal)

Premises used: Measurable.comp, ENNReal.toReal, ProbabilityTheory.IdentDistrib.comp, Measurable.pow_const, measurable_coe_nnreal_ennreal, measurable_nnnorm
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ IdentDistrib (γ := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) (fun (x : β) ↦ ‖g x‖ₑ ^ p.toReal) μ ν

Tactic:
exact h.comp (Measurable.pow_const (measurable_coe_nnreal_ennreal.comp measurable_nnnorm)
    p.toReal)

Premises used: Measurable.comp, ENNReal.toReal, ProbabilityTheory.IdentDistrib.comp, Measurable.pow_const, measurable_coe_nnreal_ennreal, measurable_nnnorm
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : BorelSpace γ
p : ℝ≥0∞
h : IdentDistrib f g μ ν
hf : MemLp f p μ
⊢ MemLp g p ν

Tactic:
⟨h.aestronglyMeasurable_snd hf.aestronglyMeasurable, ?_⟩

Premises used: ProbabilityTheory.IdentDistrib.aestronglyMeasurable_snd, MeasureTheory.MemLp, And.intro, MeasureTheory.MemLp.aestronglyMeasurable
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : BorelSpace γ
p : ℝ≥0∞
h : IdentDistrib f g μ ν
hf : MemLp f p μ
refine : eLpNorm g p ν < ∞
⊢ MemLp g p ν

Tactic:
refine ⟨h.aestronglyMeasurable_snd hf.aestronglyMeasurable, ?_⟩
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : BorelSpace γ
p : ℝ≥0∞
h : IdentDistrib f g μ ν
hf : MemLp f p μ
rw : eLpNorm f p μ < ∞
⊢ eLpNorm g p ν < ∞

Tactic:
rw [← h.eLpNorm_eq]

Premises used: ProbabilityTheory.IdentDistrib.eLpNorm_eq
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : BorelSpace γ
p : ℝ≥0∞
h : IdentDistrib f g μ ν
hf : MemLp f p μ
⊢ eLpNorm f p μ < ∞

Tactic:
hf.2

Premises used: And.right
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : BorelSpace γ
p : ℝ≥0∞
h : IdentDistrib f g μ ν
hf : MemLp f p μ
⊢ eLpNorm f p μ < ∞

Tactic:
exact hf.2

Premises used: And.right
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : BorelSpace γ
p : ℝ≥0∞
h : IdentDistrib f g μ ν
⊢ MemLp f p μ ↔ MemLp g p ν

Tactic:
⟨fun hf => h.memLp_snd hf, fun hg => h.symm.memLp_snd hg⟩

Premises used: ProbabilityTheory.IdentDistrib.memLp_snd, ProbabilityTheory.IdentDistrib.symm, Iff.intro
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : BorelSpace γ
h : IdentDistrib f g μ ν
hf : Integrable f μ
rw : ∀ (hf : MemLp f 1 μ), MemLp g 1 ν
⊢ Integrable g ν

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : BorelSpace γ
h : IdentDistrib f g μ ν
hf : MemLp f 1 μ
⊢ MemLp g 1 ν

Tactic:
h.memLp_snd hf

Premises used: ProbabilityTheory.IdentDistrib.memLp_snd
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : BorelSpace γ
h : IdentDistrib f g μ ν
hf : MemLp f 1 μ
⊢ MemLp g 1 ν

Tactic:
exact h.memLp_snd hf

Premises used: ProbabilityTheory.IdentDistrib.memLp_snd
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : BorelSpace γ
h : IdentDistrib f g μ ν
⊢ Integrable f μ ↔ Integrable g ν

Tactic:
⟨fun hf => h.integrable_snd hf, fun hg => h.symm.integrable_snd hg⟩

Premises used: ProbabilityTheory.IdentDistrib.symm, ProbabilityTheory.IdentDistrib.integrable_snd, Iff.intro
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
⊢ IdentDistrib (γ := ℝ) (fun (x : α) ↦ ‖f x‖) (fun (x : β) ↦ ‖g x‖) μ ν

Tactic:
h.comp measurable_norm

Premises used: measurable_norm, ProbabilityTheory.IdentDistrib.comp
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
⊢ IdentDistrib (γ := ℝ≥0) (fun (x : α) ↦ ‖f x‖₊) (fun (x : β) ↦ ‖g x‖₊) μ ν

Tactic:
h.comp measurable_nnnorm

Premises used: ProbabilityTheory.IdentDistrib.comp, measurable_nnnorm
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : Pow γ ℕ
inst_4 : MeasurablePow γ ℕ
h : IdentDistrib f g μ ν
n : ℕ
⊢ IdentDistrib.{u_1, u_2, u_3} (γ := γ) (fun (x : α) ↦ f x ^ n) (fun (x : β) ↦ g x ^ n) μ ν

Tactic:
h.comp (measurable_id.pow_const n)

Premises used: measurable_id, ProbabilityTheory.IdentDistrib.comp, Measurable.pow_const
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : Pow γ ℕ
inst_4 : MeasurablePow γ ℕ
h : IdentDistrib f g μ ν
⊢ IdentDistrib.{u_1, u_2, u_3} (γ := γ) (fun (x : α) ↦ HPow.hPow (β := ℕ) (f x) 2)
    (fun (x : β) ↦ HPow.hPow (β := ℕ) (g x) 2) μ ν

Tactic:
h.comp (measurable_id.pow_const 2)

Premises used: measurable_id, ProbabilityTheory.IdentDistrib.comp, OfNat.ofNat, Measurable.pow_const
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ≥0
g : β → ℝ≥0
h : IdentDistrib f g μ ν
⊢ IdentDistrib (γ := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) (fun (x : β) ↦ (↑(g x) : ℝ≥0∞)) μ ν

Tactic:
h.comp measurable_coe_nnreal_ennreal

Premises used: ENNReal.ofNNReal, ProbabilityTheory.IdentDistrib.comp, measurable_coe_nnreal_ennreal
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : Mul γ
inst_4 : MeasurableMul γ
h : IdentDistrib f g μ ν
c : γ
⊢ IdentDistrib.{u_1, u_2, u_3} (γ := γ) (fun (x : α) ↦ f x * c) (fun (x : β) ↦ g x * c) μ ν

Tactic:
h.comp (measurable_mul_const c)

Premises used: MeasurableMul.measurable_mul_const, ProbabilityTheory.IdentDistrib.comp
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : Mul γ
inst_4 : MeasurableMul γ
h : IdentDistrib f g μ ν
c : γ
⊢ IdentDistrib.{u_1, u_2, u_3} (γ := γ) (fun (x : α) ↦ c * f x) (fun (x : β) ↦ c * g x) μ ν

Tactic:
h.comp (measurable_const_mul c)

Premises used: MeasurableMul.measurable_const_mul, ProbabilityTheory.IdentDistrib.comp
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : Div γ
inst_4 : MeasurableDiv γ
h : IdentDistrib f g μ ν
c : γ
⊢ IdentDistrib.{u_1, u_2, u_3} (γ := γ) (fun (x : α) ↦ f x / c) (fun (x : β) ↦ g x / c) μ ν

Tactic:
h.comp (MeasurableDiv.measurable_div_const c)

Premises used: MeasurableDiv.measurable_div_const, ProbabilityTheory.IdentDistrib.comp
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : Div γ
inst_4 : MeasurableDiv γ
h : IdentDistrib f g μ ν
c : γ
⊢ IdentDistrib.{u_1, u_2, u_3} (γ := γ) (fun (x : α) ↦ c / f x) (fun (x : β) ↦ c / g x) μ ν

Tactic:
h.comp (MeasurableDiv.measurable_const_div c)

Premises used: MeasurableDiv.measurable_const_div, ProbabilityTheory.IdentDistrib.comp
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : Inv γ
inst_4 : MeasurableInv γ
h : IdentDistrib f g μ ν
⊢ IdentDistrib f⁻¹ g⁻¹ μ ν

Tactic:
h.comp measurable_inv

Premises used: MeasurableInv.measurable_inv, ProbabilityTheory.IdentDistrib.comp
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g μ ν
⊢ ∫⁻ (x : α), HPow.hPow (β := ℕ) (↑‖f x - ∫ (x : α), f x ∂μ‖₊ : ℝ≥0∞) 2 ∂μ =
    ∫⁻ (x : β), HPow.hPow (β := ℕ) (↑‖g x - ∫ (x : α), f x ∂μ‖₊ : ℝ≥0∞) 2 ∂ν

Tactic:
(h.sub_const (∫ x, f x ∂μ)).nnnorm.coe_nnreal_ennreal.sq.lintegral_eq

Premises used: ProbabilityTheory.IdentDistrib.coe_nnreal_ennreal, ProbabilityTheory.IdentDistrib.lintegral_eq, ProbabilityTheory.IdentDistrib.nnnorm, ProbabilityTheory.IdentDistrib.sub_const, MeasureTheory.integral, ProbabilityTheory.IdentDistrib.sq
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g μ ν
h₁ : eVar[g; ν] = ∫⁻ (x : β), HPow.hPow (β := ℕ) (↑‖g x - ∫ (x : α), f x ∂μ‖₊ : ℝ≥0∞) 2 ∂ν
⊢ eVar[f; μ] = eVar[g; ν]

Tactic:
convert! (h.sub_const (∫ x, f x ∂μ)).nnnorm.coe_nnreal_ennreal.sq.lintegral_eq

Premises used: ProbabilityTheory.IdentDistrib.coe_nnreal_ennreal, ProbabilityTheory.IdentDistrib.lintegral_eq, ProbabilityTheory.IdentDistrib.nnnorm, ProbabilityTheory.IdentDistrib.sub_const, MeasureTheory.integral, ProbabilityTheory.IdentDistrib.sq
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g μ ν
h₁ : eVar[g; ν] = ∫⁻ (x : β), HPow.hPow (β := ℕ) (↑‖g x - ∫ (x : β), g x ∂ν‖₊ : ℝ≥0∞) 2 ∂ν
⊢ eVar[g; ν] = ∫⁻ (x : β), HPow.hPow (β := ℕ) (↑‖g x - ∫ (x : α), f x ∂μ‖₊ : ℝ≥0∞) 2 ∂ν

Tactic:
rw [h.integral_eq]

Premises used: ProbabilityTheory.IdentDistrib.integral_eq
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g μ ν
⊢ eVar[g; ν] = ∫⁻ (x : β), HPow.hPow (β := ℕ) (↑‖g x - ∫ (x : β), g x ∂ν‖₊ : ℝ≥0∞) 2 ∂ν

Tactic:
rfl
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g μ ν
rw : eVar[g; ν].toReal = Var[g; ν]
⊢ Var[f; μ] = Var[g; ν]

Tactic:
rw [variance, h.evariance_eq]

Premises used: ProbabilityTheory.variance, ProbabilityTheory.IdentDistrib.evariance_eq
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g μ ν
⊢ eVar[g; ν].toReal = Var[g; ν]

Tactic:
rfl
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
⊢ UniformIntegrable f p μ

Tactic:
uniformIntegrable_of' hp hp' hfmeas fun ε hε => ?_

Premises used: MeasureTheory.uniformIntegrable_of'
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
inst : MeasurableSpace α
E : Type u_5
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
μ : Measure α
inst_4 : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
refine :
  ∀ (ε : ℝ) (hε : 0 < ε),
    ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
⊢ UniformIntegrable f p μ

Tactic:
refine uniformIntegrable_of' hp hp' hfmeas fun ε hε => ?_

Premises used: MeasureTheory.uniformIntegrable_of'