Theorems / mh_prob_7d2670

Mathlib held-out

Probability · medium

Statement, exactly as the model and Lean see it
theorem lg_target {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] {X : Ω → E} [NormedSpace ℝ E] [CompleteSpace E] [SecondCountableTopology E] (hX : ProbabilityTheory.HasGaussianLaw X P) : MeasureTheory.Integrable X P := by
Mathlib declaration
ProbabilityTheory.HasGaussianLaw.integrable
Held-out module
Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Banned modules (itself + downstream)
7
Reference proof premises (reachable / held-out)
2 / 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.00030

Attempts

  1. sample 0 · round 0Syntax error13.7 s model time
    Proof
    intros
have hX' : ∀ (s : Set E), MeasurableSet s → MeasurableSet (preimage X s)
  := by apply ProbabilityTheory.has_gaussian_law.measurable_preimage
apply MeasureTheory.Integrable.on_borel_space
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (by apply ProbabilityTheory.has_gaussian_law.integrable_on_borel_space)
  (......
    What Lean printed (this is all the model sees on repair)
    33:5: error: unexpected token '...'; expected ')', '↑', '↥', '⇑' or term
5:61: error: Unknown identifier `preimage`
3:315: error: unsolved goals
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : MeasureTheory.Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
X : Ω → E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
hX : ProbabilityTheory.HasGaussianLaw X P
⊢ MeasureTheory.Integrable X P

Reference proof

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

lemma integrable [CompleteSpace E] [SecondCountableTopology E] (hX : HasGaussianLaw X P) :
    Integrable X P :=
  memLp_one_iff_integrable.1 <| hX.memLp (by norm_num)