awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
C : ℝ≥0
hμ : ∀ᶠ (n : ℕ) in atTop, (μ n : (a : Set E) → ℝ≥0∞) Set.univ ≤ (↑C : ℝ≥0∞)
⊢ IsTightMeasureSet (Set.range μ)
have refine : ∀ (z : E) (hz : ‖z‖ = 1),
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop)
    atTop (𝓝 0)
Tactic: refine isTightMeasureSet_range_of_tendsto_limsup_inner_of_norm_eq_one 𝕜 fun z hz ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
C : ℝ≥0
hμ : ∀ᶠ (n : ℕ) in atTop, (μ n : (a : Set E) → ℝ≥0∞) Set.univ ≤ (↑C : ℝ≥0∞)
z : E
hz : ‖z‖ = 1
r : ℝ
⊢ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop =
    ENNReal.ofReal (limsup (fun (n : ℕ) ↦ ENNReal.toReal ((μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖})) atTop)
have rw : ∀ᶠ (a : ℕ) in atTop, (μ a : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖} ≤ (↑C : ℝ≥0∞)
Tactic: rw [ENNReal.ofReal_limsup_toReal (C := C)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
C : ℝ≥0
hμ : ∀ᶠ (n : ℕ) in atTop, (μ n : (a : Set E) → ℝ≥0∞) Set.univ ≤ (↑C : ℝ≥0∞)
z : E
hz : ‖z‖ = 1
r : ℝ
⊢ ∀ᶠ (a : ℕ) in atTop, (μ a : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖} ≤ (↑C : ℝ≥0∞)
have h₁ : ∀ (a : ℕ),
  Membership.mem (γ := Set ℕ)
    {x : ℕ |
      Membership.mem (γ := Set ℕ) {x : ℕ | (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) Set.univ ≤ (↑C : ℝ≥0∞)) x} x →
        Membership.mem (γ := Set ℕ)
          {x : ℕ | (fun (a : ℕ) ↦ (μ a : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖} ≤ (↑C : ℝ≥0∞)) x} x}
    a
Tactic: filter_upwards [hμ] with n hμn using (measure_mono (Set.subset_univ _)).trans hμn
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (goal)
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
C : ℝ≥0
hμ : ∀ᶠ (n : ℕ) in atTop, (μ n : (a : Set E) → ℝ≥0∞) Set.univ ≤ (↑C : ℝ≥0∞)
z : E
hz : ‖z‖ = 1
r : ℝ
h₁ :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) Set.univ ≤ (↑C : ℝ≥0∞)) x} x →
          Membership.mem (γ := Set ℕ)
            {x : ℕ | (fun (a : ℕ) ↦ (μ a : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖} ≤ (↑C : ℝ≥0∞)) x} x}
      a
⊢ ∀ᶠ (a : ℕ) in atTop, (μ a : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖} ≤ (↑C : ℝ≥0∞)
have h₂ : ∀ (a : ℕ),
  (μ a : (a : Set E) → ℝ≥0∞) Set.univ ≤ (↑C : ℝ≥0∞) → (μ a : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖} ≤ (↑C : ℝ≥0∞)
Tactic: filter_upwards [hμ] with n hμn using (measure_mono (Set.subset_univ _)).trans hμn
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.TightNormed (hypothesis)
Goal:
E : Type u_1
mE : MeasurableSpace E
inst : NormedAddCommGroup E
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h :
  ∀ (y : E),
    ‖y‖ = 1 →
      Tendsto (β := ℝ) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
C : ℝ≥0
hμ : ∀ᶠ (n : ℕ) in atTop, (μ n : (a : Set E) → ℝ≥0∞) Set.univ ≤ (↑C : ℝ≥0∞)
z : E
hz : ‖z‖ = 1
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop)
    atTop (𝓝 0)
have h_ofReal : ∀ (r : ℝ),
  limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop =
    ENNReal.ofReal (limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop)
Tactic: have h_ofReal (r : ℝ) : limsup (fun n ↦ μ n {x | r < ‖⟪z, x⟫_𝕜‖}) atTop
      = ENNReal.ofReal (limsup (fun n ↦ (μ n).real {x | r < ‖⟪z, x⟫_𝕜‖}) atTop) := by
    simp_rw [measureReal_def]
    rw [ENNReal.ofReal_limsup_toReal (C := C)]
    filter_upwards [hμ] with n hμn using (measure_mono (Set.subset_univ _)).trans hμn
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ μ.tilted f = 0
have rw : (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / 0)) = 0
Tactic: rw [Measure.tilted, integral_undef hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬AEMeasurable f μ
⊢ μ.tilted f = 0
have refine : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
Tactic: refine tilted_of_not_integrable ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬AEMeasurable f μ
⊢ ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
have suffices : ¬AEMeasurable (β := ℝ) (fun (x : α) ↦ rexp (f x)) μ
Tactic: suffices ¬ AEMeasurable (fun x ↦ exp (f x)) μ by exact fun h ↦ this h.1.aemeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h : μ = 0
⊢ (μ.tilted fun (x : α) ↦ c) = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
have inl : (Measure.tilted 0 fun (x : α) ↦ c) =
  HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((((0 : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
⊢ (μ.tilted fun (x : α) ↦ c) = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
have inr : ENNReal.ofReal (rexp c / (μ.real Set.univ * rexp c)) • μ =
  HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
Tactic: simp only [Measure.tilted, withDensity_const, integral_const, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
⊢ ENNReal.ofReal (rexp c / (μ.real Set.univ * rexp c)) • μ =
    HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
have pos : ∀ (h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ENNReal.ofReal (rexp c / (μ.real Set.univ * rexp c)) • μ =
    HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
Tactic: by_cases h_univ : μ Set.univ = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
pos :
  ∀ (h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)),
    ENNReal.ofReal (rexp c / (μ.real Set.univ * rexp c)) • μ =
      HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
⊢ ENNReal.ofReal (rexp c / (μ.real Set.univ * rexp c)) • μ =
    HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
have neg : ∀ (h_univ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ENNReal.ofReal (rexp c / (μ.real Set.univ * rexp c)) • μ =
    HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
Tactic: by_cases h_univ : μ Set.univ = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.ofReal (rexp c / (μ.real Set.univ * rexp c)) • μ =
    HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
have neg : ENNReal.ofReal (rexp c / (μ.real Set.univ * rexp c)) = ((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.ofReal (rexp c / (μ.real Set.univ * rexp c)) = ((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹
have neg : Ne (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [div_eq_mul_inv, mul_inv, mul_comm, mul_assoc, inv_mul_cancel₀ (exp_pos _).ne', mul_one,
      measureReal_def, ← ENNReal.toReal_inv, ENNReal.ofReal_toReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
⊢ (μ.tilted fun (x : α) ↦ c) = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
have x : μ = 0 ∨ NeZero μ
Tactic: cases eq_zero_or_neZero μ with
  | inl h => rw [h]; simp
  | inr h0 =>
    simp only [Measure.tilted, withDensity_const, integral_const, smul_eq_mul]
    by_cases h_univ : μ Set.univ = ∞
    · simp only [measureReal_def, h_univ, ENNReal.toReal_top, zero_mul, div_zero,
      ENNReal.ofReal_zero, zero_smul, ENNReal.inv_top]
    congr
    rw [div_eq_mul_inv, mul_inv, mul_comm, mul_assoc, inv_mul_cancel₀ (exp_pos _).ne', mul_one,
      measureReal_def, ← ENNReal.toReal_inv, ENNReal.ofReal_toReal]
    simp [h0.out]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
⊢ Eq (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) (∫ (x : α), rexp (g x) ∂μ)
have refine : (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ rexp (f x)) fun (x : α) ↦ rexp (g x)
Tactic: refine integral_congr_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ rexp (f x)) fun (x : α) ↦ rexp (g x)
have h : ∀ (x : α) (hx : f x = g x), rexp (f x) = rexp (g x)
Tactic: filter_upwards [hfg] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
x : α
hx : f x = g x
⊢ rexp (f x) = rexp (g x)
have h : rexp (g x) = rexp (g x)
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
⊢ μ.tilted f = μ.tilted g
have h_int_eq : Eq (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) (∫ (x : α), rexp (g x) ∂μ)
Tactic: have h_int_eq : ∫ x, exp (f x) ∂μ = ∫ x, exp (g x) ∂μ := by
    refine integral_congr_ae ?_
    filter_upwards [hfg] with x hx
    rw [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
h_int_eq : Eq (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) (∫ (x : α), rexp (g x) ∂μ)
⊢ μ.tilted f = μ.tilted g
have refine : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) fun (x : α) ↦
  ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ)
Tactic: refine withDensity_congr_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
h_int_eq : Eq (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) (∫ (x : α), rexp (g x) ∂μ)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) fun (x : α) ↦
    ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ)
have h : ∀ (x : α) (hx : f x = g x),
  ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) = ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ)
Tactic: filter_upwards [hfg] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
h_int_eq : Eq (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) (∫ (x : α), rexp (g x) ∂μ)
x : α
hx : f x = g x
⊢ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) = ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ)
have h : ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (g x) ∂μ) = ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ)
Tactic: rw [h_int_eq, hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
h_int_eq : Eq (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) (∫ (x : α), rexp (g x) ∂μ)
x : α
hx : f x = g x
h : ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (g x) ∂μ) = ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ)
⊢ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) = ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ)
have h₁ : ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ) = ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ)
Tactic: rw [h_int_eq, hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) =
    μ.withDensity fun (x : α) ↦ (↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) : ℝ≥0∞)
have e_f : ∀ (x : α),
  ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) =
    (↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) sorry) : ℝ≥0∞)
Tactic: congr with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
x : α
⊢ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) =
    (↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) : ℝ≥0∞)
have e_f : (↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) sorry) : ℝ≥0∞) =
  (↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) sorry) : ℝ≥0∞)
Tactic: rw [ENNReal.ofReal_eq_coe_nnreal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
x : α
e_f :
  (↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) : ℝ≥0∞) =
    (↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) : ℝ≥0∞)
⊢ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) =
    (↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) : ℝ≥0∞)
have e_f₁ : 0 ≤ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ
Tactic: rw [ENNReal.ofReal_eq_coe_nnreal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
s : Set α
hs : MeasurableSet s
⊢ (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ∂μ
have rw : (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) : (a : Set α) → ℝ≥0∞) s =
  ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ∂μ
Tactic: rw [Measure.tilted, withDensity_apply _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
s : Set α
hs : MeasurableSet s
rw :
  (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) : (a : Set α) → ℝ≥0∞) s =
    ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ∂μ
⊢ (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ∂μ
have rw₁ : ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ∂μ =
  ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ∂μ
Tactic: rw [Measure.tilted, withDensity_apply _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
s : Set α
⊢ (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ∂μ
have rw : (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) : (a : Set α) → ℝ≥0∞) s =
  ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ∂μ
Tactic: rw [Measure.tilted, withDensity_apply' _ s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
s : Set α
rw :
  (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) : (a : Set α) → ℝ≥0∞) s =
    ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ∂μ
⊢ (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ∂μ
have rw₁ : ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ∂μ =
  ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ∂μ
Tactic: rw [Measure.tilted, withDensity_apply' _ s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
⊢ (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)
have pos : ∀ (hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ),
  (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)
Tactic: by_cases hf : Integrable (fun x ↦ exp (f x)) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
pos :
  ∀ (hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ),
    (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)
⊢ (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)
have neg : ∀ (hf : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ),
  (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)
Tactic: by_cases hf : Integrable (fun x ↦ exp (f x)) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)
have pos : Integrable (ε := ℝ) (fun (a : α) ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) (μ.restrict s)
Tactic: rw [tilted_apply' _ _ hs, ← ofReal_integral_eq_lintegral_ofReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
pos : Integrable (ε := ℝ) (fun (a : α) ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) (μ.restrict s)
⊢ (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)
have pos₁ : (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ
Tactic: rw [tilted_apply' _ _ hs, ← ofReal_integral_eq_lintegral_ofReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
s : Set α
⊢ (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)
have pos : ∀ (hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ),
  (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)
Tactic: by_cases hf : Integrable (fun x ↦ exp (f x)) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
s : Set α
pos :
  ∀ (hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ),
    (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)
⊢ (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)
have neg : ∀ (hf : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ),
  (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)
Tactic: by_cases hf : Integrable (fun x ↦ exp (f x)) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
s : Set α
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)
have pos : Integrable (ε := ℝ) (fun (a : α) ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) (μ.restrict s)
Tactic: rw [tilted_apply _ _, ← ofReal_integral_eq_lintegral_ofReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
s : Set α
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
pos : Integrable (ε := ℝ) (fun (a : α) ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) (μ.restrict s)
⊢ (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)
have pos₁ : (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ
Tactic: rw [tilted_apply _ _, ← ofReal_integral_eq_lintegral_ofReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : NeZero μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ IsProbabilityMeasure (μ.tilted f)
have measure_univ : Eq (α := ℝ≥0∞) ((μ.tilted f : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : NeZero μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ Eq (α := ℝ≥0∞) ((μ.tilted f : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have measure_univ : ∫⁻ (a : α), ENNReal.ofReal (rexp (f a)) * (ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ))⁻¹ ∂μ = 1
Tactic: simp_rw [tilted_apply' _ _ MeasurableSet.univ, setLIntegral_univ,
    ENNReal.ofReal_div_of_pos (integral_exp_pos hf), div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : NeZero μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (rexp (f a)) * (ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ))⁻¹ ∂μ = 1
have measure_univ : ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ) ≠ 0
Tactic: rw [lintegral_mul_const'' _ hf.1.aemeasurable.ennreal_ofReal,
    ← ofReal_integral_eq_lintegral_ofReal hf (ae_of_all _ fun _ ↦ (exp_pos _).le),
    ENNReal.mul_inv_cancel]