Skip to content

feat: the set without arbitrage that carries a constraint null also carries a given measure, or an arbitrage charges that measure #416

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
lmlexplore-automation merged 2 commits into from
Nov 15, 2026
Merged

feat: the set without arbitrage that carries a constraint null also carries a given measure, or an arbitrage charges that measure #416

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
43e99b7
feat: the set without arbitrage that carries a constraint null also c…
RemyDegenne Nov 15, 2026
5964106
fix: name the dichotomy after the sum, and close the zero-measure cas…
RemyDegenne Nov 15, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
66 changes: 49 additions & 17 deletions LMLExplore/EValues/ConstraintNull/CompleteClass.lean
View file
Open in desktop

@RemyDegenne RemyDegenne Nov 15, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🟡 naming — request_changes claude/claude-opus-5-5

The new theorem's name says it produces a nonzero measure, but Q is an input and what the statement produces is weights ρ whose combination is positive on a set that Q charges.

  • LMLExplore/EValues/ConstraintNull/CompleteClass.lean:462 — In exists_measurableSet_noArbitrageOn_or_exists_measure_ne_zero, the suffix exists_measure_ne_zero reads as an existential over a nonzero measure. The statement actually quantifies over weights ρ : ι → ℝ and ends with Q {x | 0 < ∑ i, ρ i * g i x} ≠ 0 for the given Q. The module-doc bullet at line 70 repeats the name. Fix: Rename the existential after the sum, e.g. exists_measurableSet_noArbitrageOn_or_exists_measure_setOf_sum_mul_pos_ne_zero, or more briefly exists_measurableSet_noArbitrageOn_or_exists_sum_mul_pos, and update the module-doc bullet to match.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

claude/claude-opus-5-5 · 21s · 53.6k in (36.7k cache read, 16.9k cache write) / 1.9k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main

@RemyDegenne RemyDegenne Nov 15, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🟡 proof-quality — request_changes claude/claude-opus-5-5

The generalized induction is readable and has comments; the derived exists_measurableSet_noArbitrageOn closes its contradiction by an undocumented rfl that relies on the zero measure unfolding through its function coercion.

  • LMLExplore/EValues/ConstraintNull/CompleteClass.lean:535 — exact absurd rfl h proves (0 : Measure 𝓧) {x | …} = 0 by rfl, which relies on the zero measure unfolding through its FunLike coercion rather than on a lemma. Fix: Replace the branch with simp at h (or exact absurd (by simp) h).

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

claude/claude-opus-5-5 · 40s · 186.3k in (173.1k cache read, 13.2k cache write) / 2.9k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main

Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,11 @@ The proof here is finite-dimensional, in three steps.
measurable set `Y` that carries every member of the null and on which the constraints admit no
arbitrage: every nonnegative combination of the constraints that is nonnegative on `Y` vanishes
on `Y` (`ProbabilityTheory.NoArbitrageOn`). The removed sets are null for every member of the
null, since there the combination has a nonnegative integrand with a nonpositive integral.
null, since there the combination has a nonnegative integrand with a nonpositive integral. The
same construction, stopped at the first removed set that a given measure `Q` charges, gives
either such a set `Y` that also carries `Q`, or a nonnegative combination of the constraints,
nonnegative almost surely under the null and under `Q`, that is positive on a set of positive
`Q`-measure.
* *The finite step.* On a finite subset of `Y`, separating a compact convex hull from a closed
convex set gives the domination up to an additive `δ > 0`.
* *Compactness.* Without arbitrage, the weights whose support is not redundant
Expand Down Expand Up @@ -63,6 +67,9 @@ supported member of the null, so that e-variables are finite on `Y`.
theorem in finite-dimensional form, on a set without arbitrage.
* `ProbabilityTheory.exists_measurableSet_noArbitrageOn`: a measurable set carrying the null, on
which the constraints admit no arbitrage.
* `ProbabilityTheory.exists_measurableSet_noArbitrageOn_or_exists_sum_mul_pos`: such a set
that also carries a given measure `Q`, or a nonnegative combination of the constraints that is
positive on a set of positive `Q`-measure.
* `ProbabilityTheory.lt_top_of_isEVar_of_noArbitrageOn`: e-variables are finite on a set without
arbitrage.
* `ProbabilityTheory.forall_integral_nonpos_iff_exists_ae_le`: **the complete class theorem**
Expand Down Expand Up @@ -447,26 +454,42 @@ theorem exists_charging_family_of_noArbitrageOn (h : NoArbitrageOn a Y) {x₀ :

variable [MeasurableSpace 𝓧] {g : ι → 𝓧 → ℝ} {f : 𝓧 → ℝ} {E : 𝓧 → ℝ≥0∞}

/-- A set carrying a null generated by finitely many measurable constraints: a measurable set of
full measure for every member of the null, on which the constraints admit no arbitrage. -/
theorem exists_measurableSet_noArbitrageOn (hg : ∀ i, Measurable (g i)) :
∃ Y : Set 𝓧, MeasurableSet Y ∧ (∀ μ ∈ constraintNull (range g), μ Yᶜ = 0) ∧
NoArbitrageOn g Y := by
/-- A set carrying a null generated by finitely many measurable constraints, seen from a measure
`Q`: either a measurable set of full measure for every member of the null and for `Q`, on which the
constraints admit no arbitrage, or a nonnegative combination of the constraints that is
nonnegative almost surely under every member of the null and under `Q`, and positive on a set of
positive `Q`-measure. -/
theorem exists_measurableSet_noArbitrageOn_or_exists_sum_mul_pos
(hg : ∀ i, Measurable (g i)) (Q : Measure 𝓧) :
(∃ Y : Set 𝓧, MeasurableSet Y ∧ (∀ μ ∈ constraintNull (range g), μ Yᶜ = 0) ∧ Q Yᶜ = 0 ∧
NoArbitrageOn g Y) ∨
∃ ρ : ι → ℝ, (∀ i, 0 ≤ ρ i) ∧
(∀ μ ∈ constraintNull (range g), ∀ᵐ x ∂μ, 0 ≤ ∑ i, ρ i * g i x) ∧
(∀ᵐ x ∂Q, 0 ≤ ∑ i, ρ i * g i x) ∧ Q {x | 0 < ∑ i, ρ i * g i x} ≠ 0 := by
classical
let V : Set 𝓧 → Submodule ℝ (ι → ℝ) := fun Y ↦ Submodule.span ℝ ((fun x i ↦ g i x) '' Y)
suffices H : ∀ n : ℕ, ∀ Y : Set 𝓧, MeasurableSet Y →
(∀ μ ∈ constraintNull (range g), μ Yᶜ = 0) → Module.finrank ℝ (V Y) = n →
∃ Y : Set 𝓧, MeasurableSet Y ∧ (∀ μ ∈ constraintNull (range g), μ Yᶜ = 0) ∧
NoArbitrageOn g Y from
H _ univ MeasurableSet.univ (by simp) rfl
(∀ μ ∈ constraintNull (range g), μ Yᶜ = 0) → Q Yᶜ = 0 → Module.finrank ℝ (V Y) = n →
(∃ Y : Set 𝓧, MeasurableSet Y ∧ (∀ μ ∈ constraintNull (range g), μ Yᶜ = 0) ∧ Q Yᶜ = 0 ∧
NoArbitrageOn g Y) ∨
∃ ρ : ι → ℝ, (∀ i, 0 ≤ ρ i) ∧
(∀ μ ∈ constraintNull (range g), ∀ᵐ x ∂μ, 0 ≤ ∑ i, ρ i * g i x) ∧
(∀ᵐ x ∂Q, 0 ≤ ∑ i, ρ i * g i x) ∧ Q {x | 0 < ∑ i, ρ i * g i x} ≠ 0 from
H _ univ MeasurableSet.univ (by simp) (by simp) rfl
intro n
induction n using Nat.strong_induction_on with
| _ n ih =>
intro Y hY hμY hn
intro Y hY hμY hQY hn
by_cases hT : NoArbitrageOn g Y
· exact ⟨Y, hY, hμY, hT⟩
· exact .inl ⟨Y, hY, hμY, hQY, hT⟩
simp only [noArbitrageOn_iff, not_forall] at hT
obtain ⟨ρ, hρ0, hρY, x₀, hx₀, hne⟩ := hT
-- the combination is nonnegative almost everywhere for the measures carried by `Y`
have hnn : ∀ ν : Measure 𝓧, ν Yᶜ = 0 → ∀ᵐ x ∂ν, 0 ≤ ∑ i, ρ i * g i x := fun ν hν ↦
Filter.eventually_of_mem (mem_ae_iff.2 hν) hρY
by_cases hQρ : Q {x | 0 < ∑ i, ρ i * g i x} = 0
swap
· exact .inr ⟨ρ, hρ0, fun μ hμ ↦ hnn μ (hμY μ hμ), hnn Q hQY, hQρ⟩
set Y' := Y ∩ {x | ∑ i, ρ i * g i x ≤ 0}
have hY' : MeasurableSet Y' := hY.inter (measurableSet_le (by fun_prop) measurable_const)
have hsub : Y'ᶜ ⊆ Yᶜ ∪ {x | 0 < ∑ i, ρ i * g i x} := by
Expand All @@ -479,13 +502,12 @@ theorem exists_measurableSet_noArbitrageOn (hg : ∀ i, Measurable (g i)) :
have hμY' : ∀ μ ∈ constraintNull (range g), μ Y'ᶜ = 0 := by
intro μ hμ
have hint := integrable_sum_mul_of_mem_constraintNull hμ ρ
have hnn : 0 ≤ᵐ[μ] fun x ↦ ∑ i, ρ i * g i x :=
Filter.eventually_of_mem (mem_ae_iff.2 (hμY μ hμ)) hρY
have h0 := (integral_eq_zero_iff_of_nonneg_ae hnn hint).1
have h0 := (integral_eq_zero_iff_of_nonneg_ae (hnn μ (hμY μ hμ)) hint).1
(le_antisymm (integral_sum_mul_nonpos_of_mem_constraintNull hμ hρ0)
(integral_nonneg_of_ae hnn))
(integral_nonneg_of_ae (hnn μ (hμY μ hμ))))
refine measure_mono_null hsub (measure_union_null (hμY μ hμ) ?_)
exact measure_mono_null (fun x hx ↦ (mem_ofPred_eq ▸ hx).ne') (ae_iff.1 h0)
have hQY' : Q Y'ᶜ = 0 := measure_mono_null hsub (measure_union_null hQY hQρ)
-- removing the set where the combination is positive lowers the dimension
have hlt : V Y' < V Y := by
refine lt_of_le_of_ne (Submodule.span_mono (image_mono inter_subset_left)) fun heq ↦ ?_
Expand All @@ -500,7 +522,17 @@ theorem exists_measurableSet_noArbitrageOn (hg : ∀ i, Measurable (g i)) :
have : (fun i ↦ g i x₀) ∈ V Y := Submodule.subset_span ⟨x₀, hx₀, rfl⟩
rw [← heq] at this
exact hne (by simpa [hℓ] using hle this)
exact ih _ (hn ▸ Submodule.finrank_lt_finrank_of_lt hlt) Y' hY' hμY' rfl
exact ih _ (hn ▸ Submodule.finrank_lt_finrank_of_lt hlt) Y' hY' hμY' hQY' rfl

/-- A set carrying a null generated by finitely many measurable constraints: a measurable set of
full measure for every member of the null, on which the constraints admit no arbitrage. -/
theorem exists_measurableSet_noArbitrageOn (hg : ∀ i, Measurable (g i)) :
∃ Y : Set 𝓧, MeasurableSet Y ∧ (∀ μ ∈ constraintNull (range g), μ Yᶜ = 0) ∧
NoArbitrageOn g Y := by
obtain ⟨Y, hY, hμY, -, hT⟩ | ⟨_, -, -, -, h⟩ :=
exists_measurableSet_noArbitrageOn_or_exists_sum_mul_pos hg 0
· exact ⟨Y, hY, hμY, hT⟩
· simp at h

/-- On a set without arbitrage, an e-variable for the null is finite. -/
theorem lt_top_of_isEVar_of_noArbitrageOn (hg : ∀ i, Measurable (g i)) (hY : NoArbitrageOn g Y)
Expand Down
Loading