awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this_1 : IsFiniteMeasure μ
S : Set (Measure X) := {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this :
  ∀ {s : Set X} (hsm : MeasurableSet s) (hfs : f ⁻¹' s = s)
    (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
refine_1 :
  HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) c +
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) c =
    1
⊢ μ ∈ openSegment ℝ≥0∞ (c • μ[|s]) (c • μ[|sᶜ])
have refine_2 : HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) c • c • μ[|s] +
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) c • c • μ[|sᶜ] =
  μ
Tactic: refine ⟨μ s / c, μ sᶜ / c, ENNReal.div_pos hs hc, ENNReal.div_pos hs' hc, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this_1 : IsFiniteMeasure μ
S : Set (Measure X) := {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this :
  ∀ {s : Set X} (hsm : MeasurableSet s) (hfs : f ⁻¹' s = s)
    (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) c +
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) c =
    1
have refine_1 : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) / c = 1
Tactic: rw [← ENNReal.add_div, measure_add_measure_compl hsm, h.1.2, ENNReal.div_self hc₀ hc]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this_1 : IsFiniteMeasure μ
S : Set (Measure X) := {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this :
  ∀ {s : Set X} (hsm : MeasurableSet s) (hfs : f ⁻¹' s = s)
    (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
refine_1 :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) / c = 1
⊢ HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) c +
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) c =
    1
have refine_1₁ : HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) c = 1
Tactic: rw [← ENNReal.add_div, measure_add_measure_compl hsm, h.1.2, ENNReal.div_self hc₀ hc]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this_1 : IsFiniteMeasure μ
S : Set (Measure X) := {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this :
  ∀ {s : Set X} (hsm : MeasurableSet s) (hfs : f ⁻¹' s = s)
    (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
refine_1 :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) / c = 1
refine_1₁ : HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) c = 1
⊢ HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) c +
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) c =
    1
have refine_1₂ : c / c = 1
Tactic: rw [← ENNReal.add_div, measure_add_measure_compl hsm, h.1.2, ENNReal.div_self hc₀ hc]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this_1 : IsFiniteMeasure μ
S : Set (Measure X) := {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this :
  ∀ {s : Set X} (hsm : MeasurableSet s) (hfs : f ⁻¹' s = s)
    (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
refine_1 :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) / c = 1
refine_1₁ : HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) c = 1
refine_1₂ : c / c = 1
⊢ HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) c +
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) c =
    1
have refine_1₃ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [← ENNReal.add_div, measure_add_measure_compl hsm, h.1.2, ENNReal.div_self hc₀ hc]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (hypothesis)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this_1 : IsFiniteMeasure μ
S : Set (Measure X) := {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this :
  ∀ {s : Set X} (hsm : MeasurableSet s) (hfs : f ⁻¹' s = s)
    (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False
have hcond : c • μ[|s] = μ
Tactic: have hcond : c • μ[|s] = μ := by
      apply h.2 (this hsm hfs hs) (this hsm.compl (by rw [preimage_compl, hfs]) hs')
      refine ⟨μ s / c, μ sᶜ / c, ENNReal.div_pos hs hc, ENNReal.div_pos hs' hc, ?_, ?_⟩
      · rw [← ENNReal.add_div, measure_add_measure_compl hsm, h.1.2, ENNReal.div_self hc₀ hc]
      · simp [ProbabilityTheory.cond, smul_smul, ← mul_assoc, ENNReal.div_mul_cancel,
          ENNReal.mul_inv_cancel, *]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (hypothesis)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this_1 : IsFiniteMeasure μ
S : Set (Measure X) := {ν : Measure X | MeasurePreserving f ν ν ∧ (ν : (a : Set X) → ℝ≥0∞) univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this :
  ∀ {s : Set X} (hsm : MeasurableSet s) (hfs : f ⁻¹' s = s)
    (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hcond : c • μ[|s] = μ
⊢ False
have hs'₁ : Ne (α := ℝ≥0∞) ((c • μ[|s] : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← hcond] at hs'
Cleared hypotheses: hs', hcond
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (hypothesis)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
⊢ ∃ (c : ℝ≥0∞), ν = c • μ
have this : ν.rnDeriv μ ∘ f =ᶠ[ae μ] ν.rnDeriv μ
Tactic: have := hfν.rnDeriv_comp_aeEq hμ.toMeasurePreserving
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
this : ν.rnDeriv μ ∘ f =ᶠ[ae μ] ν.rnDeriv μ
⊢ ∃ (c : ℝ≥0∞), ν = c • μ
have obtain : ∀ (c : ℝ≥0∞) (hc : ν.rnDeriv μ =ᶠ[ae μ] const X c), ∃ (c : ℝ≥0∞), ν = c • μ
Tactic: obtain ⟨c, hc⟩ := hμ.ae_eq_const_of_ae_eq_comp₀ (measurable_rnDeriv _ _).nullMeasurable this
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
this : ν.rnDeriv μ ∘ f =ᶠ[ae μ] ν.rnDeriv μ
c : ℝ≥0∞
hc : ν.rnDeriv μ =ᶠ[ae μ] const X c
⊢ ∃ (c : ℝ≥0∞), ν = c • μ
have h : ν = c • μ
Tactic: use c
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
this : ν.rnDeriv μ ∘ f =ᶠ[ae μ] ν.rnDeriv μ
c : ℝ≥0∞
hc : ν.rnDeriv μ =ᶠ[ae μ] const X c
⊢ ν = c • μ
have h : ∀ (s : Set X) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
this : ν.rnDeriv μ ∘ f =ᶠ[ae μ] ν.rnDeriv μ
c : ℝ≥0∞
hc : ν.rnDeriv μ =ᶠ[ae μ] const X c
s : Set X
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have ν₁ : ∫⁻ (x : X) in s, c ∂μ = (c • μ : (a : Set X) → ℝ≥0∞) s
Tactic: calc
    ν s = ∫⁻ a in s, ν.rnDeriv μ a ∂μ := .symm <| setLIntegral_rnDeriv hνμ _
    _ = ∫⁻ _ in s, c ∂μ := lintegral_congr_ae <| hc.filter_mono <| ae_mono restrict_le_self
    _ = (c • μ) s := by simp
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
huniv : Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ν = μ
have rcases : ∀ (c : ℝ≥0∞) [IsFiniteMeasure (c • μ)] (hfν : MeasurePreserving f (c • μ) (c • μ)) (hνμ : c • μ ≪ μ)
  (huniv : Eq (α := ℝ≥0∞) ((c • μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)), c • μ = μ
Tactic: rcases hμ.eq_smul_of_absolutelyContinuous hfν hνμ with ⟨c, rfl⟩
Cleared hypotheses: ν, inst_1, hfν, hνμ, huniv
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
inst : IsFiniteMeasure μ
hμ : Ergodic f μ
c : ℝ≥0∞
inst_1 : IsFiniteMeasure (c • μ)
hfν : MeasurePreserving f (c • μ) (c • μ)
hνμ : c • μ ≪ μ
huniv : Eq (α := ℝ≥0∞) ((c • μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ c • μ = μ
have inl : ∀ [IsFiniteMeasure.{u_1} (α := X) (m0 := m) 0] (hμ : Ergodic (m := m) f 0)
  [IsFiniteMeasure (HSMul.hSMul (β := Measure X) c 0)]
  (hfν : MeasurePreserving f (HSMul.hSMul (β := Measure X) c 0) (HSMul.hSMul (β := Measure X) c 0))
  (hνμ : HSMul.hSMul (β := Measure X) c 0 ≪ 0)
  (huniv :
    Eq (α := ℝ≥0∞) ((HSMul.hSMul (β := Measure X) c 0 : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
      (((0 : Measure X) : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)),
  HSMul.hSMul (β := Measure X) c 0 = 0
Tactic: rcases eq_or_ne μ 0 with rfl | hμ₀
Cleared hypotheses: μ, inst, hμ, inst_1, hfν, hνμ, huniv
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
inst : IsFiniteMeasure μ
hμ : Ergodic f μ
c : ℝ≥0∞
inst_1 : IsFiniteMeasure (c • μ)
hfν : MeasurePreserving f (c • μ) (c • μ)
hνμ : c • μ ≪ μ
huniv : Eq (α := ℝ≥0∞) ((c • μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
inl :
  ∀ [IsFiniteMeasure.{u_1} (α := X) (m0 := m) 0] (hμ : Ergodic (m := m) f 0)
    [IsFiniteMeasure (HSMul.hSMul (β := Measure X) c 0)]
    (hfν : MeasurePreserving f (HSMul.hSMul (β := Measure X) c 0) (HSMul.hSMul (β := Measure X) c 0))
    (hνμ : HSMul.hSMul (β := Measure X) c 0 ≪ 0)
    (huniv :
      Eq (α := ℝ≥0∞) ((HSMul.hSMul (β := Measure X) c 0 : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
        (((0 : Measure X) : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)),
    HSMul.hSMul (β := Measure X) c 0 = 0
⊢ c • μ = μ
have inr : ∀ (hμ₀ : μ ≠ 0), c • μ = μ
Tactic: rcases eq_or_ne μ 0 with rfl | hμ₀
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
inst : IsFiniteMeasure μ
hμ : Ergodic f μ
⊢ Membership.mem (γ := Set (Measure X))
      {ν : Measure X |
        MeasurePreserving f ν ν ∧
          Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)}
      μ ∧
    ∀ (x₁ : Measure X),
      Membership.mem (γ := Set (Measure X))
          {ν : Measure X |
            MeasurePreserving f ν ν ∧
              Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)}
          x₁ →
        ∀ (x₂ : Measure X),
          Membership.mem (γ := Set (Measure X))
              {ν : Measure X |
                MeasurePreserving f ν ν ∧
                  Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)}
              x₂ →
            μ ∈ openSegment ℝ≥0∞ x₁ x₂ → x₁ = μ
have refine : ∀ (x₁ : Measure X),
  Membership.mem (γ := Set (Measure X))
      {ν : Measure X |
        MeasurePreserving f ν ν ∧
          Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)}
      x₁ →
    ∀ (x₂ : Measure X),
      Membership.mem (γ := Set (Measure X))
          {ν : Measure X |
            MeasurePreserving f ν ν ∧
              Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)}
          x₂ →
        μ ∈ openSegment ℝ≥0∞ x₁ x₂ → x₁ = μ
Tactic: refine ⟨⟨hμ.toMeasurePreserving, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
f : X → X
ν₁ : Measure X
hfν₁ : MeasurePreserving f ν₁ ν₁
ν₂ : Measure X
hfν₂ : MeasurePreserving f ν₂ ν₂
a b : ℝ≥0∞
ha : 0 < a
hb : 0 < b
hab : a + b = 1
inst : IsFiniteMeasure (a • ν₁ + b • ν₂)
hμ : Ergodic f (a • ν₁ + b • ν₂)
hν₁μ : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((a • ν₁ + b • ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
hν₂μ : Eq (α := ℝ≥0∞) ((ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((a • ν₁ + b • ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((ν₁ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞) ((a • ν₁ + b • ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [hν₁μ]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (hypothesis)
Goal:
X : Type u_1
m : MeasurableSpace X
f : X → X
ν₁ : Measure X
hfν₁ : MeasurePreserving f ν₁ ν₁
ν₂ : Measure X
hfν₂ : MeasurePreserving f ν₂ ν₂
a b : ℝ≥0∞
ha : 0 < a
hb : 0 < b
hab : a + b = 1
inst : IsFiniteMeasure (a • ν₁ + b • ν₂)
hμ : Ergodic f (a • ν₁ + b • ν₂)
hν₁μ : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((a • ν₁ + b • ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
hν₂μ : Eq (α := ℝ≥0∞) ((ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((a • ν₁ + b • ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ν₁ = a • ν₁ + b • ν₂
have this : IsFiniteMeasure ν₁
Tactic: have : IsFiniteMeasure ν₁ := ⟨by rw [hν₁μ]; apply measure_lt_top⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Extreme (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
f : X → X
ν₁ : Measure X
hfν₁ : MeasurePreserving f ν₁ ν₁
ν₂ : Measure X
hfν₂ : MeasurePreserving f ν₂ ν₂
a b : ℝ≥0∞
ha : 0 < a
hb : 0 < b
hab : a + b = 1
inst : IsFiniteMeasure (a • ν₁ + b • ν₂)
hμ : Ergodic f (a • ν₁ + b • ν₂)
hν₁μ : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((a • ν₁ + b • ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
hν₂μ : Eq (α := ℝ≥0∞) ((ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ((a • ν₁ + b • ν₂ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν₁
⊢ ν₁ = a • ν₁ + b • ν₂
have apply : ν₁ ≪ a • ν₁
Tactic: apply hμ.eq_of_absolutelyContinuous_measure_univ_eq hfν₁ (.add_right _ _) hν₁μ
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Function (goal)
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : Nonempty X
inst_2 : MeasurableSpace X
s : Set X
inst_3 : MeasurableSpace.CountablySeparated.{u_2} (↑s : Type u_2)
f : α → α
g : α → X
h : QuasiErgodic f μ
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
⊢ ∃ (c : X), g =ᶠ[ae μ] const α c
have refine : ∀ (U : Set X), MeasurableSet U → (∀ᵐ (x : α) ∂μ, g x ∈ U) ∨ ∀ᵐ (x : α) ∂μ, g x ∉ U
Tactic: refine exists_eventuallyEq_const_of_eventually_mem_of_forall_separating MeasurableSet hs ?_
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Function (goal)
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : Nonempty X
inst_2 : MeasurableSpace X
s : Set X
inst_3 : MeasurableSpace.CountablySeparated.{u_2} (↑s : Type u_2)
f : α → α
g : α → X
h : QuasiErgodic f μ
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
⊢ ∀ (U : Set X), MeasurableSet U → (∀ᵐ (x : α) ∂μ, g x ∈ U) ∨ ∀ᵐ (x : α) ∂μ, g x ∉ U
have _b : ∀ (U : Set X) (hU : MeasurableSet U), f ⁻¹' g ⁻¹' U =ᶠ[ae μ] g ⁻¹' U
Tactic: refine fun U hU ↦ h.ae_mem_or_ae_notMem₀ (s := g ⁻¹' U) (hgm hU) ?_b
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Function (goal)
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : Nonempty X
inst_2 : MeasurableSpace X
s : Set X
inst_3 : MeasurableSpace.CountablySeparated.{u_2} (↑s : Type u_2)
f : α → α
g : α → X
h : QuasiErgodic f μ
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
U : Set X
hU : MeasurableSet U
⊢ f ⁻¹' g ⁻¹' U =ᶠ[ae μ] g ⁻¹' U
have _b : ∀ (x : α) (hx : (g ∘ f) x = g x), x ∈ f ⁻¹' g ⁻¹' U ↔ x ∈ g ⁻¹' U
Tactic: refine (hg_eq.mono fun x hx ↦ ?_).set_eq
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Function (goal)
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : Nonempty X
inst_2 : MeasurableSpace X
s : Set X
inst_3 : MeasurableSpace.CountablySeparated.{u_2} (↑s : Type u_2)
f : α → α
g : α → X
h : QuasiErgodic f μ
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
U : Set X
hU : MeasurableSet U
x : α
hx : (g ∘ f) x = g x
⊢ x ∈ f ⁻¹' g ⁻¹' U ↔ x ∈ g ⁻¹' U
have _b : x ∈ g ∘ f ⁻¹' U ↔ x ∈ g ⁻¹' U
Tactic: rw [← preimage_comp, mem_preimage, mem_preimage, hx]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Function (goal)
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : Nonempty X
inst_2 : MeasurableSpace X
s : Set X
inst_3 : MeasurableSpace.CountablySeparated.{u_2} (↑s : Type u_2)
f : α → α
g : α → X
h : QuasiErgodic f μ
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
U : Set X
hU : MeasurableSet U
x : α
hx : (g ∘ f) x = g x
_b : x ∈ g ∘ f ⁻¹' U ↔ x ∈ g ⁻¹' U
⊢ x ∈ f ⁻¹' g ⁻¹' U ↔ x ∈ g ⁻¹' U
have _b₁ : (g ∘ f) x ∈ U ↔ x ∈ g ⁻¹' U
Tactic: rw [← preimage_comp, mem_preimage, mem_preimage, hx]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Function (goal)
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : Nonempty X
inst_2 : MeasurableSpace X
s : Set X
inst_3 : MeasurableSpace.CountablySeparated.{u_2} (↑s : Type u_2)
f : α → α
g : α → X
h : QuasiErgodic f μ
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
U : Set X
hU : MeasurableSet U
x : α
hx : (g ∘ f) x = g x
_b : x ∈ g ∘ f ⁻¹' U ↔ x ∈ g ⁻¹' U
_b₁ : (g ∘ f) x ∈ U ↔ x ∈ g ⁻¹' U
⊢ x ∈ f ⁻¹' g ⁻¹' U ↔ x ∈ g ⁻¹' U
have _b₂ : (g ∘ f) x ∈ U ↔ g x ∈ U
Tactic: rw [← preimage_comp, mem_preimage, mem_preimage, hx]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Function (goal)
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : Nonempty X
inst_2 : MeasurableSpace X
s : Set X
inst_3 : MeasurableSpace.CountablySeparated.{u_2} (↑s : Type u_2)
f : α → α
g : α → X
h : QuasiErgodic f μ
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
U : Set X
hU : MeasurableSet U
x : α
hx : (g ∘ f) x = g x
_b : x ∈ g ∘ f ⁻¹' U ↔ x ∈ g ⁻¹' U
_b₁ : (g ∘ f) x ∈ U ↔ x ∈ g ⁻¹' U
_b₂ : (g ∘ f) x ∈ U ↔ g x ∈ U
⊢ x ∈ f ⁻¹' g ⁻¹' U ↔ x ∈ g ⁻¹' U
have _b₃ : g x ∈ U ↔ g x ∈ U
Tactic: rw [← preimage_comp, mem_preimage, mem_preimage, hx]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Function (goal)
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : Nonempty X
inst_2 : MeasurableSpace X
inst_3 : MeasurableSpace.CountablySeparated X
f : α → α
g : α → X
h : PreErgodic f μ
hgm : Measurable g
hg_eq : g ∘ f = g
U : Set X
hU : MeasurableSet U
⊢ f ⁻¹' g ⁻¹' U = g ⁻¹' U
have rw : g ∘ f ⁻¹' U = g ⁻¹' U
Tactic: rw [← preimage_comp, hg_eq]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Function (goal)
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : Nonempty X
inst_2 : MeasurableSpace X
inst_3 : MeasurableSpace.CountablySeparated X
f : α → α
g : α → X
h : PreErgodic f μ
hgm : Measurable g
hg_eq : g ∘ f = g
U : Set X
hU : MeasurableSet U
rw : g ∘ f ⁻¹' U = g ⁻¹' U
⊢ f ⁻¹' g ⁻¹' U = g ⁻¹' U
have rw₁ : g ⁻¹' U = g ⁻¹' U
Tactic: rw [← preimage_comp, hg_eq]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Function (hypothesis)
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace X
inst_2 : MetrizableSpace X
inst_3 : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f μ
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
⊢ ∃ (c : X), g =ᶠ[ae μ] const α c
have this : let this := borel X;
BorelSpace X
Tactic: borelize X
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Function (goal)
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace X
inst_2 : MetrizableSpace X
inst_3 : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f μ
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
⊢ ∃ (c : X), g =ᶠ[ae μ] const α c
have rcases : ∀ (t : Set X) (ht : IsSeparable t) (hgt : ∀ᵐ (x : α) ∂μ, g x ∈ t), ∃ (c : X), g =ᶠ[ae μ] const α c
Tactic: rcases hgm.isSeparable_ae_range with ⟨t, ht, hgt⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Function (hypothesis)
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace X
inst_2 : MetrizableSpace X
inst_3 : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f μ
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
t : Set X
ht : IsSeparable t
hgt : ∀ᵐ (x : α) ∂μ, g x ∈ t
⊢ ∃ (c : X), g =ᶠ[ae μ] const α c
have this : SecondCountableTopology.{u_2} (↑t : Type u_2)
Tactic: haveI := ht.secondCountableTopology
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f f' : α → β
hf : MeasurePreserving f μa μb
hf' : Measurable f'
h : f =ᶠ[ae μa] f'
⊢ MeasurePreserving f' μa μb
have refine : map f' μa = μb
Tactic: refine ⟨hf', ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f f' : α → β
hf : MeasurePreserving f μa μb
hf' : Measurable f'
h : f =ᶠ[ae μa] f'
⊢ map f' μa = μb
have rw : map f μa = μb
Tactic: rw [Measure.map_congr h.symm]