awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) ≤
    HSMul.hSMul (β := ℝ≥0∞) n ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
have zero : (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[0] ⁻¹' s)) ≤
  HSMul.hSMul (α := ℕ) (β := ℝ≥0∞) 0 ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    simp only [add_smul, one_smul]
    grw [← ih, measure_symmDiff_le s (f^[n] ⁻¹' s) (f^[n + 1] ⁻¹' s)]
    replace hs : NullMeasurableSet (s ∆ (f ⁻¹' s)) μ :=
      hs.symmDiff <| hs.preimage hf.quasiMeasurePreserving
    rw [iterate_succ', preimage_comp, ← preimage_symmDiff, (hf.iterate n).measure_preimage hs]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
zero :
  (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[0] ⁻¹' s)) ≤
    HSMul.hSMul (α := ℕ) (β := ℝ≥0∞) 0 ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) ≤
    HSMul.hSMul (β := ℝ≥0∞) n ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
have succ : ∀ (n : ℕ)
  (ih :
    (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) ≤
      HSMul.hSMul (β := ℝ≥0∞) n ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)),
  (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n + 1] ⁻¹' s)) ≤
    HSMul.hSMul (β := ℝ≥0∞) (n + 1) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    simp only [add_smul, one_smul]
    grw [← ih, measure_symmDiff_le s (f^[n] ⁻¹' s) (f^[n + 1] ⁻¹' s)]
    replace hs : NullMeasurableSet (s ∆ (f ⁻¹' s)) μ :=
      hs.symmDiff <| hs.preimage hf.quasiMeasurePreserving
    rw [iterate_succ', preimage_comp, ← preimage_symmDiff, (hf.iterate n).measure_preimage hs]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
have A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
Tactic: have A : ∀ m, NullMeasurableSet (f^[m] ⁻¹' s) μ := fun m ↦
    hs.preimage (hf.iterate m).quasiMeasurePreserving
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
have B : ∀ (m : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: have B : ∀ m, μ (f^[m] ⁻¹' s) = μ s := fun m ↦ (hf.iterate m).measure_preimage hs
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
B : ∀ (m : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
have this : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
  (∑ m ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞)
Tactic: have : μ (univ : Set α) < ∑ m ∈ Finset.range n, μ (f^[m] ⁻¹' s) := by simpa [B]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
B : ∀ (m : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
this :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
    (∑ m ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞)
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
have obtain : ∀ (i : ℕ) (hi : i < n) (j : ℕ) (hj : j < n) (hij : i ≠ j) (x : α) (hxi : f^[i] x ∈ s) (hxj : f^[j] x ∈ s),
  ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
Tactic: obtain ⟨i, hi, j, hj, hij, x, hxi : f^[i] x ∈ s, hxj : f^[j] x ∈ s⟩ :
      ∃ i < n, ∃ j < n, i ≠ j ∧ (f^[i] ⁻¹' s ∩ f^[j] ⁻¹' s).Nonempty := by
    simpa using exists_nonempty_inter_of_measure_univ_lt_sum_measure μ (fun m _ ↦ A m) this
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
B : ∀ (m : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
this :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
    (∑ m ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞)
i : ℕ
hi : i < n
j : ℕ
hj : j < n
hij : i ≠ j
x : α
hxi : f^[i] x ∈ s
hxj : f^[j] x ∈ s
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
have inr : ∀
  (this :
    ∀ (i : ℕ) (hi : i < n) (j : ℕ) (hj : j < n) (hij : i ≠ j) (hxi : f^[i] x ∈ s) (hxj : f^[j] x ∈ s) (hlt : i < j),
      ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s)
  (hlt : ¬i < j), ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
Tactic: wlog hlt : i < j generalizing i j
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
B : ∀ (m : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
this :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
    (∑ m ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞)
i : ℕ
hi : i < n
j : ℕ
hj : j < n
hij : i ≠ j
x : α
hxi : f^[i] x ∈ s
hxj : f^[j] x ∈ s
inr :
  ∀
    (this :
      ∀ (i : ℕ) (hi : i < n) (j : ℕ) (hj : j < n) (hij : i ≠ j) (hxi : f^[i] x ∈ s) (hxj : f^[j] x ∈ s) (hlt : i < j),
        ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s)
    (hlt : ¬i < j), ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
have wlog : ∀ (i : ℕ) (hi : i < n) (j : ℕ) (hj : j < n) (hij : i ≠ j) (hxi : f^[i] x ∈ s) (hxj : f^[j] x ∈ s) (hlt : i < j),
  ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
Tactic: wlog hlt : i < j generalizing i j
Cleared hypotheses: i, hi, j, hj, hij, hxi, hxj
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
B : ∀ (m : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
this :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
    (∑ m ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞)
x : α
i : ℕ
hi : i < n
j : ℕ
hj : j < n
hij : i ≠ j
hxi : f^[i] x ∈ s
hxj : f^[j] x ∈ s
hlt : i < j
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
have refine : f^[j - i] (f^[i] x) ∈ s
Tactic: refine ⟨f^[i] x, hxi, j - i, ⟨tsub_pos_of_lt hlt, lt_of_le_of_lt (j.sub_le i) hj⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
B : ∀ (m : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
this :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
    (∑ m ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞)
x : α
i : ℕ
hi : i < n
j : ℕ
hj : j < n
hij : i ≠ j
hxi : f^[i] x ∈ s
hxj : f^[j] x ∈ s
hlt : i < j
⊢ f^[j - i] (f^[i] x) ∈ s
have rwa : f^[j - i + i] x ∈ s
Tactic: rwa [← iterate_add_apply, tsub_add_cancel_of_le hlt.le]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
inst_1 : IsFiniteMeasure μ
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[m] x ∈ s
have rcases : ∀ (N : ℕ)
  (hN :
    (μ : (a : Set α) → ℝ≥0∞) univ <
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑N : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
  ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[m] x ∈ s
Tactic: rcases ENNReal.exists_nat_mul_gt hs' (measure_ne_top μ (Set.univ : Set α)) with ⟨N, hN⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
inst_1 : IsFiniteMeasure μ
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
N : ℕ
hN :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑N : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[m] x ∈ s
have rcases : ∀ (x : α) (hx : x ∈ s) (m : ℕ) (hm : m ∈ Ioo 0 N) (hmx : f^[m] x ∈ s), ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[m] x ∈ s
Tactic: rcases hf.exists_mem_iterate_mem_of_measure_univ_lt_mul_measure hs hN with ⟨x, hx, m, hm, hmx⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
⊢ MeasurePreserving f (μ.singularPart ν) (μ.singularPart ν)
have rcases : ∀ (s : Set X) (hsm : MeasurableSet s) (hνs : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal))
  (hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)),
  MeasurePreserving f (μ.singularPart ν) (μ.singularPart ν)
Tactic: rcases (μ.mutuallySingular_singularPart ν).symm with ⟨s, hsm, hνs, hμs⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)
hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
⊢ MeasurePreserving f (μ.singularPart ν) (μ.singularPart ν)
have h : μ.singularPart ν = μ.restrict (f ⁻¹' s)
Tactic: convert! hfμ.restrict_preimage hsm using 1
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)
hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
h : μ.singularPart ν = μ.restrict (f ⁻¹' s)
⊢ MeasurePreserving f (μ.singularPart ν) (μ.singularPart ν)
have h₁ : μ.singularPart ν = μ.restrict s
Tactic: convert! hfμ.restrict_preimage hsm using 1
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)
hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
⊢ μ.singularPart ν = μ.restrict (f ⁻¹' s)
have h : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s)ᶜ : ENNReal) (0 : ENNReal)
Tactic: refine singularPart_eq_restrict ?_ (hfν.preimage_null hνs)
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)
hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s)ᶜ : ENNReal) (0 : ENNReal)
have h : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
  ((μ.singularPart ν : (a : Set X) → ENNReal) univ : ENNReal)
Tactic: rw [← mem_ae_iff, ← Filter.eventuallyEq_univ,
      ae_eq_univ_iff_measure_eq (hfμ.measurable hsm).nullMeasurableSet]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (hypothesis)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)
hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
have hνs₁ : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal) (0 : ENNReal)
Tactic: rw [← hfν.measure_preimage hsm.nullMeasurableSet] at hνs
Cleared hypotheses: hνs, hμs
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal) (0 : ENNReal)
hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
have rw : (μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) =
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
Tactic: rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal) (0 : ENNReal)
hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
rw :
  (μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) =
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
⊢ Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
have rw₁ : (μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) =
  HAdd.hAdd (α := ENNReal) (β := ENNReal) (0 : ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
Tactic: rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal) (0 : ENNReal)
hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
rw :
  (μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) =
    HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
rw₁ :
  (μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) =
    HAdd.hAdd (α := ENNReal) (β := ENNReal) (0 : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
⊢ Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
have rw₂ : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
  ((μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
Tactic: rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)
hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
have rw : Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal) ((μ : (a : Set X) → ENNReal) s : ENNReal)
Tactic: rw [rnDeriv_add_singularPart, hfμ.measure_preimage hsm.nullMeasurableSet]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)
hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
rw : Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal) ((μ : (a : Set X) → ENNReal) s : ENNReal)
⊢ Eq (α := ENNReal) ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) (f ⁻¹' s) : ENNReal)
    ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
have rw₁ : Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) s : ENNReal) ((μ : (a : Set X) → ENNReal) s : ENNReal)
Tactic: rw [rnDeriv_add_singularPart, hfμ.measure_preimage hsm.nullMeasurableSet]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)
hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
have rw : HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
  (μ.singularPart ν : (a : Set X) → ENNReal) s
Tactic: rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)
hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
rw :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    (μ.singularPart ν : (a : Set X) → ENNReal) s
⊢ Eq (α := ENNReal) ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
have rw₁ : HAdd.hAdd (α := ENNReal) (β := ENNReal) (0 : ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
  (μ.singularPart ν : (a : Set X) → ENNReal) s
Tactic: rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)
hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
rw :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν.withDensity (μ.rnDeriv ν) : (a : Set X) → ENNReal) s : ENNReal)
      ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    (μ.singularPart ν : (a : Set X) → ENNReal) s
rw₁ :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) (0 : ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal) =
    (μ.singularPart ν : (a : Set X) → ENNReal) s
⊢ Eq (α := ENNReal) ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
have rw₂ : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
  ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
Tactic: rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.RadonNikodym (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : Eq (α := ENNReal) ((ν : (a : Set X) → ENNReal) s : ENNReal) (0 : ENNReal)
hμs : Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) univ : ENNReal)
have rw : (μ.singularPart ν : (a : Set X) → ENNReal) s =
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((μ.singularPart ν : (a : Set X) → ENNReal) s : ENNReal)
    ((μ.singularPart ν : (a : Set X) → ENNReal) sᶜ : ENNReal)
Tactic: rw [← measure_add_measure_compl hsm, hμs, add_zero]