-
Notifications
You must be signed in to change notification settings - Fork 7
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
ledger verify: an aborted sweep reports success with an inflated verified count
difficulty:smallStraightforward change for someone familiar with the repoStraightforward change for someone familiar with the repostatus:readyScoped enough for a contributor to pick upScoped enough for a contributor to pick uptype:refactorStructure or naming change that should preserve behaviorStructure or naming change that should preserve behaviorStatus: Open.#202 In formal-applied-math/formal-mathfin;docker: compose project name collides with sibling repos, silently sharing the olean volume
difficulty:smallStraightforward change for someone familiar with the repoStraightforward change for someone familiar with the repostatus:readyScoped enough for a contributor to pick upScoped enough for a contributor to pick uptype:refactorStructure or naming change that should preserve behaviorStructure or naming change that should preserve behaviorStatus: Open.#201 In formal-applied-math/formal-mathfin;Let bracketMeasure earn its name: E[(M_b − M_a)²] = ⟨M⟩((a,b]×Ω)
area:foundationsFoundations/ — Itô, Brownian motion, stochastic integration, martingales, Poisson, Markov, SDEsFoundations/ — Itô, Brownian motion, stochastic integration, martingales, Poisson, Markov, SDEsdifficulty:mediumRequires repo context, Lean fluency, or careful validationRequires repo context, Lean fluency, or careful validationstatus:readyScoped enough for a contributor to pick upScoped enough for a contributor to pick uptype:proofLean theorem, proof repair, or theorem generalizationLean theorem, proof repair, or theorem generalizationStatus: Open.#200 In formal-applied-math/formal-mathfin;Collapse simpleAssembly_T into simpleAssemblyOfMeasure (the general one has the better proof)
area:foundationsFoundations/ — Itô, Brownian motion, stochastic integration, martingales, Poisson, Markov, SDEsFoundations/ — Itô, Brownian motion, stochastic integration, martingales, Poisson, Markov, SDEsdifficulty:mediumRequires repo context, Lean fluency, or careful validationRequires repo context, Lean fluency, or careful validationstatus:readyScoped enough for a contributor to pick upScoped enough for a contributor to pick uptype:refactorStructure or naming change that should preserve behaviorStructure or naming change that should preserve behaviorStatus: Open.#199 In formal-applied-math/formal-mathfin;Instantiate Degenne's IsStochasticIntegral for the integral against an Itô integral (blocked: v4.33.0 is RC)
area:foundationsFoundations/ — Itô, Brownian motion, stochastic integration, martingales, Poisson, Markov, SDEsFoundations/ — Itô, Brownian motion, stochastic integration, martingales, Poisson, Markov, SDEsdifficulty:mediumRequires repo context, Lean fluency, or careful validationRequires repo context, Lean fluency, or careful validationstatus:blocked-upstreamBlocked on Mathlib, BrownianMotion, or another external projectBlocked on Mathlib, BrownianMotion, or another external projecttype:refactorStructure or naming change that should preserve behaviorStructure or naming change that should preserve behaviorStatus: Open.#196 In formal-applied-math/formal-mathfin;Drift term in the Itô-process price: S = S₀ + ∫b ds + (σ●B)
area:fixed-incomeFixedIncome/ — bonds, term structure, and interest-rate modelsFixedIncome/ — bonds, term structure, and interest-rate modelsarea:foundationsFoundations/ — Itô, Brownian motion, stochastic integration, martingales, Poisson, Markov, SDEsFoundations/ — Itô, Brownian motion, stochastic integration, martingales, Poisson, Markov, SDEsdifficulty:mediumRequires repo context, Lean fluency, or careful validationRequires repo context, Lean fluency, or careful validationstatus:readyScoped enough for a contributor to pick upScoped enough for a contributor to pick uptype:proofLean theorem, proof repair, or theorem generalizationLean theorem, proof repair, or theorem generalizationStatus: Open.#194 In formal-applied-math/formal-mathfin;gate the CONTRIBUTING '## Result' header rule in tests/test_router.py
type:proofLean theorem, proof repair, or theorem generalizationLean theorem, proof repair, or theorem generalizationStatus: Open.#187 In formal-applied-math/formal-mathfin;Compose the two PricesGainsAtZero guards (needs the general-integrand Itô process as a bundled Martingale)
area:foundationsFoundations/ — Itô, Brownian motion, stochastic integration, martingales, Poisson, Markov, SDEsFoundations/ — Itô, Brownian motion, stochastic integration, martingales, Poisson, Markov, SDEsdifficulty:mediumRequires repo context, Lean fluency, or careful validationRequires repo context, Lean fluency, or careful validationstatus:readyScoped enough for a contributor to pick upScoped enough for a contributor to pick uptype:proofLean theorem, proof repair, or theorem generalizationLean theorem, proof repair, or theorem generalizationStatus: Open.#186 In formal-applied-math/formal-mathfin;DRY backlog from the martingale-representation reviews: mulBddCLM, inner_eq_integral_mul, the MGF block
area:foundationsFoundations/ — Itô, Brownian motion, stochastic integration, martingales, Poisson, Markov, SDEsFoundations/ — Itô, Brownian motion, stochastic integration, martingales, Poisson, Markov, SDEsdifficulty:smallStraightforward change for someone familiar with the repoStraightforward change for someone familiar with the repostatus:readyScoped enough for a contributor to pick upScoped enough for a contributor to pick uptype:refactorStructure or naming change that should preserve behaviorStructure or naming change that should preserve behaviorStatus: Open.#185 In formal-applied-math/formal-mathfin;Drop the spurious
s 0 = 0hypothesis fromstepDoleans_sub_one_mem_rangearea:foundationsFoundations/ — Itô, Brownian motion, stochastic integration, martingales, Poisson, Markov, SDEsFoundations/ — Itô, Brownian motion, stochastic integration, martingales, Poisson, Markov, SDEsdifficulty:smallStraightforward change for someone familiar with the repoStraightforward change for someone familiar with the repostatus:readyScoped enough for a contributor to pick upScoped enough for a contributor to pick uptype:refactorStructure or naming change that should preserve behaviorStructure or naming change that should preserve behaviorStatus: Open.#184 In formal-applied-math/formal-mathfin;L¹/H¹ martingale representation, and Clark–Ocone (the named integrand)
area:foundationsFoundations/ — Itô, Brownian motion, stochastic integration, martingales, Poisson, Markov, SDEsFoundations/ — Itô, Brownian motion, stochastic integration, martingales, Poisson, Markov, SDEsdifficulty:hardRequires deep domain knowledge or upstream coordinationRequires deep domain knowledge or upstream coordinationstatus:blocked-upstreamBlocked on Mathlib, BrownianMotion, or another external projectBlocked on Mathlib, BrownianMotion, or another external projecttype:researchOpen investigation where the path is not yet clearOpen investigation where the path is not yet clearStatus: Open.#182 In formal-applied-math/formal-mathfin;Second FTAP, the converse: unique martingale measure ⟹ complete
area:foundationsFoundations/ — Itô, Brownian motion, stochastic integration, martingales, Poisson, Markov, SDEsFoundations/ — Itô, Brownian motion, stochastic integration, martingales, Poisson, Markov, SDEsdifficulty:hardRequires deep domain knowledge or upstream coordinationRequires deep domain knowledge or upstream coordinationstatus:blocked-designBlocked on a modeling, theorem-shape, or architecture decisionBlocked on a modeling, theorem-shape, or architecture decisiontype:researchOpen investigation where the path is not yet clearOpen investigation where the path is not yet clearStatus: Open.#181 In formal-applied-math/formal-mathfin;