Theorems / mh_prob_381e5e

Mathlib held-out

Probability · easy

Statement, exactly as the model and Lean see it
theorem lg_target {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : AnalyticOn ℝ (ProbabilityTheory.cgf X μ) (interior (ProbabilityTheory.integrableExpSet X μ)) := by
Mathlib declaration
ProbabilityTheory.analyticOn_cgf
Held-out module
Mathlib.Probability.Moments.MGFAnalytic
Banned modules (itself + downstream)
18
Reference proof premises (reachable / held-out)
1 / 1

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Not verified1 model calls · 1 Lean checks · $0.00097

Attempts

  1. sample 0 · round 0Lean 3 syntax48.2 s model time
    Proof
    ```lean
intro x₀
apply analytic_on_iff.1
intros ε hε
obtain ⟨δ, δ_pos, δ_le⟩ := measure_theory.measure.nnreal.exists_pos_lt_measure_ball (μ) ε
let δ' := δ / 2
have δ'_pos : 0 < δ' := by simp [δ']
have δ'_le : δ' ≤ δ := by simp [δ']
have δ'_le' : δ' ≤ ε := by rw [δ']; exact δ_le
let U := ball x₀ δ'
have U_open : is_open U := by simp [U]
have U_subset : U ⊆ ball x₀ δ := by simp [U, δ']
have U_subset_integrable : U ⊆ interior (integrable_exp_set X μ) :=
  by intro x; apply subset_interior.2; intro h; apply h
let f := λ x, (ProbabilityTheory.cgf X μ) x
let g := λ x, (ProbabilityTaylor.exp_moments X μ).exp_moment x
have g_continuous : continuous_on g (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_exp_moment
have g_eq_f : ∀ x ∈ interior (integrable_exp_set X μ), g x = f x :=
  by intro x hx; rw [ProbabilityTheory.cgf_def, ProbabilityTaylor.exp_moment_def]; rfl
let h := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h_cont : continuous_on h (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h'_cont : continuous_on h' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h'' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h''_cont : continuous_on h'' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h'''_cont : continuous_on h''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h'''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h''''_cont : continuous_on h'''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h''''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h'''''_cont : continuous_on h''''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h'''''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h''''''_cont : continuous_on h'''''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h''''''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h'''''''_cont : continuous_on h''''''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h'''''''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h''''''''_cont : continuous_on h'''''''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h''''''''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h'''''''''_cont : continuous_on h''''''''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h'''''''''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h''''''''''_cont : continuous_on h'''''''''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h''''''''''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h'''''''''''_cont : continuous_on h''''''''''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h'''''''''''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h''''''''''''_cont : continuous_on h'''''''''''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h''''''''''''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h'''''''''''''_cont : continuous_on h''''''''''''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h'''''''''''''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h''''''''''''''_cont : continuous_on h'''''''''''''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h''''''''''''''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h'''''''''''''''_cont : continuous_on h''''''''''''''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h'''''''''''''''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h''''''''''''''''_cont : continuous_on h'''''''''''''''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h''''''''''''''''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h'''''''''''''''''_cont : continuous_on h''''''''''''''''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h'''''''''''''''''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h''''''''''''''''''_cont : continuous_on h'''''''''''''''''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h''''''''''''''''''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h'''''''''''''''''''_cont : continuous_on h''''''''''''''''''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h'''''''''''''''''''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h''''''''''''''''''''_cont : continuous_on h'''''''''''''''''''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h''''''''''''''''''''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h'''''''''''''''''''''_cont : continuous_on h''''''''''''''''''''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h'''''''''''''''''''''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h''''''''''''''''''''''_cont : continuous_on h'''''''''''''''''''''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h''''''''''''''''''''''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h'''''''''''''''''''''''_cont : continuous_on h''''''''''''''''''''''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h'''''''''''''''''''''''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h''''''''''''''''''''''''_cont : continuous_on h'''''''''''''''''''''''' (interior (integrable_exp_set X μ)) :=
  by apply continuous_on_integrable_exp_set
let h''''''''''''''''''''''''' := λ x, (ProbabilityTheory.integrableExpSet X μ) x
have h'''''''''''''''''''''''''_cont : continuous_on h''''''''''''''''''''''''' (interior (integr
    What Lean printed (this is all the model sees on repair)
    3:197: error: unsolved goals
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : MeasureTheory.Measure Ω
⊢ AnalyticOn ℝ (ProbabilityTheory.cgf X μ) (interior (ProbabilityTheory.integrableExpSet X μ))
4:2: error: unexpected token '`'; expected command

Reference proof

Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.

/-- The cumulant-generating function is analytic on the interior of the interval
  `integrableExpSet X μ`. -/
lemma analyticOn_cgf : AnalyticOn ℝ (cgf X μ) (interior (integrableExpSet X μ)) :=
  analyticOnNhd_cgf.analyticOn