awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 (m₀ := inst_2) id (Measure.map f μ)
have rw : AEMeasurable (_m := inst_2) id (Measure.map f μ) ∧ ∃ (t : Set γ), IsSeparable t ∧ ∀ᵐ (x : γ) ∂Measure.map f μ, id x ∈ t
Tactic: rw [aestronglyMeasurable_iff_aemeasurable_separable]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 μ
⊢ AEMeasurable (_m := inst_2) id (Measure.map f μ) ∧
    ∃ (t : Set γ), IsSeparable t ∧ ∀ᵐ (x : γ) ∂Measure.map f μ, id x ∈ t
have rcases : ∀ (t : Set γ) (t_sep : IsSeparable t) (ht : ∀ᵐ (x : α) ∂μ, f x ∈ t),
  AEMeasurable (_m := inst_2) id (Measure.map f μ) ∧
    ∃ (t : Set γ), IsSeparable t ∧ ∀ᵐ (x : γ) ∂Measure.map f μ, id x ∈ t
Tactic: rcases (aestronglyMeasurable_iff_aemeasurable_separable.1 hf).2 with ⟨t, t_sep, ht⟩
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ AEMeasurable (_m := inst_2) id (Measure.map f μ) ∧
    ∃ (t : Set γ), IsSeparable t ∧ ∀ᵐ (x : γ) ∂Measure.map f μ, id x ∈ t
have refine : ∀ᵐ (x : γ) ∂Measure.map f μ, id x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
Tactic: refine ⟨aemeasurable_id, ⟨closure t, t_sep.closure, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ ∀ᵐ (x : γ) ∂Measure.map f μ, id x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
have rw : ∀ᵐ (x : α) ∂μ, id (f x) ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
Tactic: rw [ae_map_iff h.aemeasurable_fst]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
rw : ∀ᵐ (x : α) ∂μ, id (f x) ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ∀ᵐ (x : γ) ∂Measure.map f μ, id x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
have rw₁ : MeasurableSet.{u_3} (α := γ) {x : γ | id x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t}
Tactic: rw [ae_map_iff h.aemeasurable_fst]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ ∀ᵐ (x : α) ∂μ, id (f x) ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ t) x} x →
        Membership.mem (γ := Set α)
          {x : α | (fun (x : α) ↦ id (f x) ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t) x} x}
    a
Tactic: filter_upwards [ht] with x hx using subset_closure hx
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ t) x} x →
          Membership.mem (γ := Set α)
            {x : α | (fun (x : α) ↦ id (f x) ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t) x} x}
      a
⊢ ∀ᵐ (x : α) ∂μ, id (f x) ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
have h₂ : ∀ (a : α), f a ∈ t → id (f a) ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
Tactic: filter_upwards [ht] with x hx using subset_closure hx
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (hypothesis)
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 μ
⊢ Eq.{u_3 + 1} (α := γ) (∫ (x : α), f x ∂μ) (∫ (x : β), g x ∂ν)
have A : AEStronglyMeasurable (m₀ := inst_2) id (Measure.map f μ)
Tactic: have A : AEStronglyMeasurable id (Measure.map f μ) := by
      rw [aestronglyMeasurable_iff_aemeasurable_separable]
      rcases (aestronglyMeasurable_iff_aemeasurable_separable.1 hf).2 with ⟨t, t_sep, ht⟩
      refine ⟨aemeasurable_id, ⟨closure t, t_sep.closure, ?_⟩⟩
      rw [ae_map_iff h.aemeasurable_fst]
      · filter_upwards [ht] with x hx using subset_closure hx
      · exact isClosed_closure.measurableSet
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 μ)
⊢ Eq.{u_3 + 1} (α := γ) (∫ (x : α), f x ∂μ) (∫ (x : β), g x ∂ν)
have pos : Eq.{u_3 + 1} (α := γ) (∫ (x : α), id (f x) ∂μ) (∫ (x : β), id (g x) ∂ν)
Tactic: change ∫ x, id (f x) ∂μ = ∫ x, id (g x) ∂ν
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 μ)
⊢ Eq.{u_3 + 1} (α := γ) (∫ (x : α), id (f x) ∂μ) (∫ (x : β), id (g x) ∂ν)
have pos : Eq (α := γ) (@integral _ _ _ _ inst_2 (Measure.map f μ) fun (y : γ) ↦ id y) (∫ (x : β), id (g x) ∂ν)
Tactic: rw [← integral_map h.aemeasurable_fst A]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (hypothesis)
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 μ)
⊢ Eq (α := γ) (@integral _ _ _ _ inst_2 (Measure.map f μ) fun (y : γ) ↦ id y) (∫ (x : β), id (g x) ∂ν)
have A₁ : AEStronglyMeasurable (m₀ := inst_2) id (Measure.map g ν)
Tactic: rw [h.map_eq] at A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 ν)
⊢ Eq (α := γ) (@integral _ _ _ _ inst_2 (Measure.map f μ) fun (y : γ) ↦ id y) (∫ (x : β), id (g x) ∂ν)
have pos : Eq (α := γ) (@integral _ _ _ _ inst_2 (Measure.map f μ) fun (y : γ) ↦ id y)
  (@integral _ _ _ _ inst_2 (Measure.map g ν) fun (y : γ) ↦ id y)
Tactic: rw [← integral_map h.aemeasurable_snd A, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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)
⊢ Eq (α := γ) (@integral _ _ _ _ inst_2 (Measure.map f μ) fun (y : γ) ↦ id y) (∫ (x : β), id (g x) ∂ν)
have pos₁ : Eq (α := γ) (@integral _ _ _ _ inst_2 (Measure.map g ν) fun (y : γ) ↦ id y)
  (@integral _ _ _ _ inst_2 (Measure.map g ν) fun (y : γ) ↦ id y)
Tactic: rw [← integral_map h.aemeasurable_snd A, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 μ
⊢ Eq.{u_3 + 1} (α := γ) (∫ (x : α), f x ∂μ) (∫ (x : β), g x ∂ν)
have neg : Eq.{u_3 + 1} (α := γ) 0 (∫ (x : β), g x ∂ν)
Tactic: rw [integral_non_aestronglyMeasurable hf]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (hypothesis)
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 μ
⊢ Eq.{u_3 + 1} (α := γ) 0 (∫ (x : β), g x ∂ν)
have hf₁ : ¬AEStronglyMeasurable g ν
Tactic: rw [h.aestronglyMeasurable_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 ν
⊢ Eq.{u_3 + 1} (α := γ) 0 (∫ (x : β), g x ∂ν)
have neg : Eq.{u_3 + 1} (α := γ) 0 0
Tactic: rw [integral_non_aestronglyMeasurable hf]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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∞
⊢ eLpNorm f p μ = eLpNorm g p ν
have pos : ∀ (h0 : p = 0), eLpNorm f p μ = eLpNorm g p ν
Tactic: by_cases h0 : p = 0
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 ν
⊢ eLpNorm f p μ = eLpNorm g p ν
have neg : ∀ (h0 : ¬p = 0), eLpNorm f p μ = eLpNorm g p ν
Tactic: by_cases h0 : p = 0
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 ν
have pos : ∀ (h_top : p = ∞), eLpNorm f p μ = eLpNorm g p ν
Tactic: by_cases h_top : p = ∞
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 ν
⊢ eLpNorm f p μ = eLpNorm g p ν
have neg : ∀ (h_top : ¬p = ∞), eLpNorm f p μ = eLpNorm g p ν
Tactic: by_cases h_top : p = ∞
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 = ∞
⊢ eLpNorm f p μ = eLpNorm g p ν
have pos : Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) (essSup (fun (x : β) ↦ ‖g x‖ₑ) ν)
Tactic: simp only [h_top, eLpNorm, eLpNormEssSup, ENNReal.top_ne_zero, if_true,
      if_false]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 = ∞
⊢ Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) (essSup (fun (x : β) ↦ ‖g x‖ₑ) ν)
have pos : IdentDistrib (γ := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : β) ↦ ‖g x‖ₑ) μ ν
Tactic: apply essSup_eq
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 = ∞
⊢ eLpNorm f p μ = eLpNorm g p ν
have neg : (∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ = (∫⁻ (a : β), ‖g a‖ₑ ^ p.toReal ∂ν) ^ p.toReal⁻¹
Tactic: simp only [eLpNorm_eq_eLpNorm' h0 h_top, eLpNorm', one_div]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 = ∞
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ = (∫⁻ (a : β), ‖g a‖ₑ ^ p.toReal ∂ν) ^ p.toReal⁻¹
have neg : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ = ∫⁻ (a : β), ‖g a‖ₑ ^ p.toReal ∂ν
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 = ∞
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ = ∫⁻ (a : β), ‖g a‖ₑ ^ p.toReal ∂ν
have neg : IdentDistrib (γ := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) (fun (x : β) ↦ ‖g x‖ₑ ^ p.toReal) μ ν
Tactic: apply lintegral_eq
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 ν
have refine : eLpNorm g p ν < ∞
Tactic: refine ⟨h.aestronglyMeasurable_snd hf.aestronglyMeasurable, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 g p ν < ∞
have rw : eLpNorm f p μ < ∞
Tactic: rw [← h.eLpNorm_eq]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 μ
⊢ Integrable g ν
have rw : ∀ (hf : MemLp f 1 μ), MemLp g 1 ν
Tactic: rw [← memLp_one_iff_integrable] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g μ ν
⊢ eVar[f; μ] = eVar[g; ν]
have h₁ : eVar[g; ν] = ∫⁻ (x : β), HPow.hPow (β := ℕ) (↑‖g x - ∫ (x : α), f x ∂μ‖₊ : ℝ≥0∞) 2 ∂ν
Tactic: convert! (h.sub_const (∫ x, f x ∂μ)).nnnorm.coe_nnreal_ennreal.sq.lintegral_eq
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 : α), f x ∂μ‖₊ : ℝ≥0∞) 2 ∂ν
have h₁ : eVar[g; ν] = ∫⁻ (x : β), HPow.hPow (β := ℕ) (↑‖g x - ∫ (x : β), g x ∂ν‖₊ : ℝ≥0∞) 2 ∂ν
Tactic: rw [h.integral_eq]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g μ ν
⊢ Var[f; μ] = Var[g; ν]
have rw : eVar[g; ν].toReal = Var[g; ν]
Tactic: rw [variance, h.evariance_eq]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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 μ
have refine : ∀ (ε : ℝ) (hε : 0 < ε),
  ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
Tactic: refine uniformIntegrable_of' hp hp' hfmeas fun ε hε => ?_
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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) μ μ
ε : ℝ
hε : 0 < ε
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
have pos : ∀ (hι : Nonempty ι), ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
Tactic: by_cases hι : Nonempty ι
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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) μ μ
ε : ℝ
hε : 0 < ε
pos :
  ∀ (hι : Nonempty ι),
    ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
have neg : ∀ (hι : ¬Nonempty ι),
  ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
Tactic: by_cases hι : Nonempty ι
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
have pos : ∀ (C : ℝ) (hC₁ : 0 < C) (hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε),
  ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨C, hC₁, hC₂⟩ := hℒp.eLpNorm_indicator_norm_ge_pos_le (hfmeas _) hε
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} {x : α | C ≤ ‖f i x‖}
have h : ∀ (x : α),
  Membership.mem (γ := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C sorry ≤ ‖f i x‖₊} x ↔
    Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
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) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm (Set.indicator {x : α | C ≤ (↑‖f j x‖₊ : ℝ)} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
⊢ Membership.mem (γ := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯ ≤ ‖f i x‖₊} x ↔
    Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖} x
have h : Membership.mem (γ := Set α) {x : α | Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C sorry ≤ ‖f i x‖.toNNReal} x ↔
  Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖} x
Tactic: simp_rw [← norm_toNNReal]