Probability · medium

Statement, exactly as the model and Lean see it

theorem lg_target {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E] (h : ∀ (x : E), μ ≠ MeasureTheory.Measure.dirac x) : MeasureTheory.NullSingletonClass μ := by

Mathlib declaration: ProbabilityTheory.IsGaussian.noAtoms
Held-out module: Mathlib.Probability.Distributions.Gaussian.Fernique
Banned modules (itself + downstream): 10
Reference proof premises (reachable / held-out): 0 / 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.00029

Attempts

sample 0 · round 0Syntax error11.9 s model time

Proof

have := ProbabilityTheory.isGaussian_has_density μ
obtain ⟨f, hf⟩ := this
have := MeasureTheory.has_density_ae f hf
have := MeasureTheory.ae_eq_ae_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq_measure μ (MeasureTheory.ae_eq......

What Lean printed (this is all the model sees on repair)

7:1988: error: unexpected token '...'; expected term
4:10: error: Unknown identifier `ProbabilityTheory.isGaussian_has_density`
3:309: error: unsolved goals
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : MeasureTheory.Measure E
inst✝² : ProbabilityTheory.IsGaussian μ
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
h : ∀ (x : E), μ ≠ MeasureTheory.Measure.dirac x
⊢ MeasureTheory.NullSingletonClass μ

Reference proof

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

@[deprecated (since := "2026-06-09")]
alias noAtoms := nullSingletonClass