awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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 : ℝ
n : ℕ
hμn : (μ n : (a : Set E) → ℝ≥0∞) Set.univ ≤ (↑C : ℝ≥0∞)
⊢ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖} ≤ (↑C : ℝ≥0∞)

Tactic:
(measure_mono (Set.subset_univ _)).trans hμn

Premises used: Set.subset_univ, MeasureTheory.measure_mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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
h₂ h₃ :
  ∀ (n : ℕ) (hμn : (μ n : (a : Set E) → ℝ≥0∞) Set.univ ≤ (↑C : ℝ≥0∞)),
    (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖} ≤ (↑C : ℝ≥0∞)
⊢ ∀ᶠ (a : ℕ) in atTop, (μ 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
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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 : ℕ) ↦ (μ 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
-- Module: Mathlib.MeasureTheory.Measure.TightNormed
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
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)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n : (a : Set E) → ℝ≥0∞) {x : E | r < ‖⟪z, x⟫_𝕜‖}) atTop)
    atTop (𝓝 0)

Tactic:
simpa only [h_ofReal, ← ENNReal.ofReal_zero] using ENNReal.tendsto_ofReal (h z hz)

Premises used: ENNReal.ofReal_zero, ENNReal.tendsto_ofReal
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
rw : (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / 0)) = 0
⊢ μ.tilted f = 0

Tactic:
rw [Measure.tilted, integral_undef hf]

Premises used: MeasureTheory.integral_undef, MeasureTheory.Measure.tilted
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / 0)) = 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬AEMeasurable f μ
⊢ μ.tilted f = 0

Tactic:
tilted_of_not_integrable ?_

Premises used: MeasureTheory.tilted_of_not_integrable
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬AEMeasurable f μ
refine : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ μ.tilted f = 0

Tactic:
refine tilted_of_not_integrable ?_

Premises used: MeasureTheory.tilted_of_not_integrable
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬AEMeasurable f μ
this : ¬AEMeasurable (β := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ

Tactic:
fun h ↦ this h.1.aemeasurable

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, And.left, Not
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬AEMeasurable f μ
this : ¬AEMeasurable (β := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ

Tactic:
exact fun h ↦ this h.1.aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬AEMeasurable f μ
suffices : ¬AEMeasurable (β := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ

Tactic:
suffices ¬ AEMeasurable (fun x ↦ exp (f x)) μ by exact fun h ↦ this h.1.aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬AEMeasurable f μ
⊢ ¬AEMeasurable (β := ℝ) (fun (x : α) ↦ rexp (f x)) μ

Tactic:
fun h ↦ hf (aemeasurable_of_aemeasurable_exp h)

Premises used: Real.aemeasurable_of_aemeasurable_exp, Not
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬AEMeasurable f μ
⊢ ¬AEMeasurable (β := ℝ) (fun (x : α) ↦ rexp (f x)) μ

Tactic:
exact fun h ↦ hf (aemeasurable_of_aemeasurable_exp h)

Premises used: Real.aemeasurable_of_aemeasurable_exp
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
⊢ Eq (α := Measure α) (Measure.tilted 0 f) 0

Tactic:
simp [Measure.tilted]

Premises used: MeasureTheory.Measure.tilted
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h : μ = 0
inl :
  (Measure.tilted 0 fun (x : α) ↦ c) =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((((0 : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) 0
⊢ (μ.tilted fun (x : α) ↦ c) = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h : μ = 0
⊢ (Measure.tilted 0 fun (x : α) ↦ c) =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((((0 : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
inr :
  ENNReal.ofReal (rexp c / (μ.real Set.univ * rexp c)) • μ =
    HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
⊢ (μ.tilted fun (x : α) ↦ c) = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ

Tactic:
simp only [Measure.tilted, withDensity_const, integral_const, smul_eq_mul]

Premises used: MeasureTheory.Measure.tilted, MeasureTheory.integral_const, smul_eq_mul, MeasureTheory.withDensity_const
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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∞) μ
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∞) μ
⊢ 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 = ∞

Premises used: Set.univ, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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∞) μ

Tactic:
simp only [measureReal_def, h_univ, ENNReal.toReal_top, zero_mul, div_zero,
      ENNReal.ofReal_zero, zero_smul, ENNReal.inv_top]

Premises used: MulZeroClass.zero_mul, zero_smul, ENNReal.ofReal_zero, MeasureTheory.measureReal_def, ENNReal.inv_top, ENNReal.toReal_top, div_zero
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
neg : ENNReal.ofReal (rexp c / (μ.real Set.univ * rexp c)) = ((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹
⊢ ENNReal.ofReal (rexp c / (μ.real Set.univ * rexp c)) • μ =
    HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
neg : Ne (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.ofReal (rexp c / (μ.real Set.univ * rexp c)) = ((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹

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]

Premises used: mul_inv, mul_assoc, ENNReal.toReal_inv, ENNReal.ofReal_toReal, div_eq_mul_inv, LT.lt.ne', mul_comm, MeasureTheory.measureReal_def, mul_one, inv_mul_cancel₀, Real.exp_pos
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [h0.out]

Premises used: NeZero.out
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
⊢ μ = 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]

Premises used: mul_inv, Set.univ, MulZeroClass.zero_mul, mul_assoc, ENNReal.toReal_inv, ENNReal.ofReal_toReal, div_eq_mul_inv, MeasureTheory.Measure.tilted, LT.lt.ne', zero_smul, MeasureTheory.integral_const, mul_comm, ENNReal.ofReal_zero, MeasureTheory.measureReal_def, ENNReal.inv_top, smul_eq_mul, mul_one, ENNReal.toReal_top, MeasureTheory.withDensity_const, DFunLike.coe, inv_mul_cancel₀, eq_zero_or_neZero, div_zero, Real.exp_pos
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsProbabilityMeasure μ
c : ℝ
⊢ (μ.tilted fun (x : α) ↦ c) = μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ (μ.tilted fun (x : α) ↦ 0) = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsProbabilityMeasure μ
⊢ μ.tilted 0 = μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
⊢ Eq (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) (∫ (x : α), rexp (g x) ∂μ)

Tactic:
integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
refine : (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ rexp (f x)) fun (x : α) ↦ rexp (g x)
⊢ Eq (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) (∫ (x : α), rexp (g x) ∂μ)

Tactic:
refine integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
h : ∀ (x : α) (hx : f x = g x), rexp (f x) = rexp (g x)
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ rexp (f x)) fun (x : α) ↦ rexp (g x)

Tactic:
filter_upwards [hfg] with x hx
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
x : α
hx : f x = g x
h h₁ : rexp (g x) = rexp (g x)
⊢ rexp (f x) = rexp (g x)

Tactic:
rw [hx]
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hfg : f =ᶠ[ae μ] g
⊢ 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]
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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

Tactic:
withDensity_congr_ae ?_

Premises used: MeasureTheory.Measure.tilted, MeasureTheory.withDensity_congr_ae
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂μ)
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) ∂μ)
⊢ μ.tilted f = μ.tilted g

Tactic:
refine withDensity_congr_ae ?_

Premises used: MeasureTheory.withDensity_congr_ae
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂μ)
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) ∂μ)
⊢ (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:
filter_upwards [hfg] with x hx
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂μ)
h₁ h₂ : ENNReal.ofReal (rexp (g 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) ∂μ)

Tactic:
rw [h_int_eq, hx]
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ_1 : Measure α
f_1 : α → ℝ
μ : Measure α
f : α → ℝ
x : α
⊢ 0 ≤ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
e_f :
  ∀ (x : α),
    ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) =
      (↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) : ℝ≥0∞)
⊢ (μ.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∞)

Tactic:
congr with x
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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∞)
e_f₁ : 0 ≤ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ
e_f₂ :
  (↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) : ℝ≥0∞) =
    (↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) : ℝ≥0∞)
e_f₃ : 0 ≤ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ
⊢ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) =
    (↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) : ℝ≥0∞)

Tactic:
rw [ENNReal.ofReal_eq_coe_nnreal]

Premises used: ENNReal.ofReal_eq_coe_nnreal
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂μ) ∂μ
rw₁ 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) ∂μ) ∂μ
⊢ (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ∂μ

Tactic:
rw [Measure.tilted, withDensity_apply _ hs]

Premises used: MeasureTheory.Measure.tilted, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂μ) ∂μ
rw₁ 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) ∂μ) ∂μ
⊢ (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ∂μ

Tactic:
rw [Measure.tilted, withDensity_apply' _ s]

Premises used: MeasureTheory.Measure.tilted, MeasureTheory.withDensity_apply'
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂μ ∂μ)
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) ∂μ ∂μ)
⊢ (μ.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)) μ

Premises used: MeasureTheory.Integrable, Real.exp
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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)
pos₁ : (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ 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) ∂μ ∂μ)

Tactic:
rw [tilted_apply' _ _ hs, ← ofReal_integral_eq_lintegral_ofReal]

Premises used: MeasureTheory.ofReal_integral_eq_lintegral_ofReal, MeasureTheory.tilted_apply'
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) (μ.restrict s)

Tactic:
hf.integrableOn.div_const _

Premises used: MeasureTheory.Integrable.div_const, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) (μ.restrict s)

Tactic:
exact hf.integrableOn.div_const _

Premises used: MeasureTheory.Integrable.div_const, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
x : α
⊢ LE.le (α := ℝ) (0 x) ((fun (a : α) ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) x)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
exact ae_of_all _ (fun _ ↦ by positivity)

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂μ ∂μ)

Tactic:
simp only [hf, not_false_eq_true, tilted_of_not_integrable, Measure.coe_zero,
      Pi.zero_apply, integral_undef hf, div_zero, integral_zero, ENNReal.ofReal_zero]

Premises used: MeasureTheory.integral_undef, Pi.zero_apply, MeasureTheory.tilted_of_not_integrable, ENNReal.ofReal_zero, not_false_eq_true, MeasureTheory.integral_zero, div_zero, MeasureTheory.Measure.coe_zero
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂μ ∂μ)
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) ∂μ ∂μ)
⊢ (μ.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)) μ

Premises used: MeasureTheory.Integrable, Real.exp