/- Copyright (c) 2026 Raphael Coelho. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Raphael Coelho -/ import MathFin /-! # Axiom audit — the "axioms-clean" claim, build-enforced The library's headline claim is that every `full` derivation is `#print axioms`-clean: it depends only on the three standard Mathlib axioms `[propext, Classical.choice, Quot.sound]` — no `sorryAx`, no extra axioms. This file turns that claim from a docstring assertion (in `docs/coverage.md`) into a **build-enforced invariant**. Each `#guard_msgs in #print axioms` block below pins the axiom dependencies of a headline / load-bearing theorem. If any audited theorem ever picks up `sorryAx` (a `sorry` slipped in) or a new axiom (a dependency changed), the `#guard_msgs` check fails and **the build breaks**. The audited set spans every area of the library — it is representative, not exhaustive; extend it when a new load-bearing theorem lands. A theorem that appears here is certified axioms-clean by `lake build`, not by assertion. Note: pure-algebra theorems (closed by `ring`/`field_simp`) may legitimately depend on a *subset* of the three (or none); those are pinned to their actual set below. The invariant we enforce is "no `sorryAx`, no axiom outside the standard three", which the pinned messages capture exactly. -/ namespace MathFin.AxiomAudit /-! ## Black-Scholes core -/ /-- info: 'MathFin.bs_call_formula' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.bs_call_formula /-- info: 'MathFin.bsP_eq_bsV' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.bsP_eq_bsV /-- info: 'MathFin.hasDerivAt_bsV_S' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.hasDerivAt_bsV_S /-- info: 'MathFin.bs_pde_holds' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.bs_pde_holds /-- info: 'MathFin.expected_terminal_eq_forward' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.expected_terminal_eq_forward /-! ## Feynman–Kac → Black–Scholes-PDE keystone -/ /-- info: 'MathFin.FeynmanKacHeatEquation.feynmanU_heat_equation' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.FeynmanKacHeatEquation.feynmanU_heat_equation /-- info: 'MathFin.bsV_satisfies_bs_pde_via_feynmanKac' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.bsV_satisfies_bs_pde_via_feynmanKac /-! ## Garman normal form + consumer-side corollaries -/ /-- info: 'MathFin.bsV_eq_bsVGarman_standard' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.bsV_eq_bsVGarman_standard /-- info: 'MathFin.black_futures_price_eq_bsVGarman' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.black_futures_price_eq_bsVGarman /-- info: 'MathFin.bs_dividends_price_eq_bsVGarman' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.bs_dividends_price_eq_bsVGarman /-! ## Gaussian MGF + lognormal moments -/ /-- info: 'MathFin.integral_exp_affine_gaussianPDFReal_univ' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.integral_exp_affine_gaussianPDFReal_univ /-- info: 'MathFin.nthMoment_terminal' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.nthMoment_terminal /-- info: 'MathFin.secondMoment_terminal' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.secondMoment_terminal /-- info: 'MathFin.variance_terminal' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.variance_terminal /-- info: 'MathFin.bsLogReturn_mean' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.bsLogReturn_mean /-! ## Exponential-discount principle + the rate-recovery retrofits -/ /-- info: 'MathFin.rate_eq_neg_log_deriv' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.rate_eq_neg_log_deriv /-- info: 'MathFin.forwardRate_eq_neg_log_discount' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.forwardRate_eq_neg_log_discount /-- info: 'MathFin.force_eq_neg_log_deriv_survival' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.force_eq_neg_log_deriv_survival /-- info: 'MathFin.hazard_eq_neg_log_deriv_survival' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.hazard_eq_neg_log_deriv_survival /-! ## Static Girsanov: the risk-neutral measure derived -/ /-- info: 'MathFin.gaussian_esscher_pdf' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.gaussian_esscher_pdf /-- info: 'MathFin.gaussianReal_withDensity_esscher' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.gaussianReal_withDensity_esscher /-- info: 'MathFin.BSCallHyp.exists_of_physical' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.BSCallHyp.exists_of_physical /-- info: 'MathFin.bsTerminal_physical_eq_riskNeutral' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.bsTerminal_physical_eq_riskNeutral /-- info: 'MathFin.discounted_terminal_eq_S0_of_physical' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.discounted_terminal_eq_S0_of_physical /-- info: 'MathFin.bs_call_formula_of_physical' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.bs_call_formula_of_physical /-- info: 'MathFin.discounted_physical_terminal_eq_S0' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.discounted_physical_terminal_eq_S0 /-! ## Margrabe exchange option (first multivariate result) -/ /-- info: 'MathFin.margrabe_effective_variance' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.margrabe_effective_variance /-- info: 'MathFin.exchange_payoff_eq_ratio' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.exchange_payoff_eq_ratio /-- info: 'MathFin.margrabe_eq_bsVGarman' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.margrabe_eq_bsVGarman /-- info: 'MathFin.margrabe_parity' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.margrabe_parity /-- info: 'MathFin.margrabe_price_via_call' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.margrabe_price_via_call /-! ## Convex pricing functional + FTAP / state-price wiring -/ /-- info: 'MathFin.statePricePricing_convexOn' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.statePricePricing_convexOn /-- info: 'MathFin.callPrice_finiteState_butterfly_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.callPrice_finiteState_butterfly_nonneg /-- info: 'MathFin.stateprice_call_butterfly_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.stateprice_call_butterfly_nonneg /-! ## Binomial trees -/ /-- info: 'MathFin.americanCallPrice_le_binomialPrice' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.americanCallPrice_le_binomialPrice /-! ## Variance swap (QV limit) -/ /-- info: 'MathFin.tendsto_expected_bsLogPrice_equipartition_sum' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.tendsto_expected_bsLogPrice_equipartition_sum /-! ## L² quadratic variation of Brownian motion (Summit 1) + its in-probability corollary -/ /-- info: 'MathFin.QuadraticVariationL2.tendsto_qv' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.QuadraticVariationL2.tendsto_qv /-- info: 'MathFin.QuadraticVariationL2.tendstoInMeasure_qv' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.QuadraticVariationL2.tendstoInMeasure_qv /-- info: 'MathFin.BrownianQuadraticVariation.qv_equals_t' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.BrownianQuadraticVariation.qv_equals_t /-! ## Expectation-form Itô / Feynman–Kac (the QV → ½f″ correction, from first principles) -/ /-- info: 'MathFin.FeynmanKacHeatEquation.heatConvolution_eq_add_integral_deriv' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.FeynmanKacHeatEquation.heatConvolution_eq_add_integral_deriv /-- info: 'MathFin.FeynmanKacHeatEquation.expectation_ito' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.FeynmanKacHeatEquation.expectation_ito /-- info: 'MathFin.FeynmanKacHeatEquation.expectation_ito_isPreBrownian' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.FeynmanKacHeatEquation.expectation_ito_isPreBrownian /-! ## Adapted Itô isometry (increment-independence cornerstone) -/ /-- info: 'MathFin.ItoIsometryAdapted.integral_adapted_mul_increment' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.ItoIsometryAdapted.integral_adapted_mul_increment /-- info: 'MathFin.ItoIsometryAdapted.integral_adapted_sq_mul_increment_sq' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIsometryAdapted.integral_adapted_sq_mul_increment_sq /-- info: 'MathFin.ItoIsometryAdapted.ito_isometry_discrete' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.ItoIsometryAdapted.ito_isometry_discrete /-- info: 'MathFin.ItoIsometryAdapted.ito_isometry_brownian_self' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.ItoIsometryAdapted.ito_isometry_brownian_self /-- info: 'MathFin.ItoIsometryAdapted.integral_adapted_mul_increment_sq' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIsometryAdapted.integral_adapted_mul_increment_sq /-- info: 'MathFin.ItoIsometryAdapted.ito_isometry_discrete_bilinear' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIsometryAdapted.ito_isometry_discrete_bilinear /-! ## Predictable-rectangle pairing (inner-product core of the continuous Itô integral) -/ /-- info: 'MathFin.ItoIsometryAdapted.adapted_indepFun_forward' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIsometryAdapted.adapted_indepFun_forward /-- info: 'MathFin.ItoIsometryAdapted.integral_two_increment' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIsometryAdapted.integral_two_increment /-- info: 'MathFin.ItoIsometryAdapted.rect_increment_pairing' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIsometryAdapted.rect_increment_pairing /-! ## Continuous Itô integral — foundational bridge (AdaptedAt ↔ natural filtration) -/ /-- info: 'MathFin.ItoIntegralL2.adaptedAt_of_measurable_natural' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralL2.adaptedAt_of_measurable_natural /-! ## Continuous Itô integral as a CLM on `[0,T]` — the headline -/ /-- info: 'MathFin.ItoIntegralCLM.generateFrom_predictableRect' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralCLM.generateFrom_predictableRect /-- info: 'MathFin.ItoIntegralCLM.assembly_isometry_T' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralCLM.assembly_isometry_T /-- info: 'MathFin.ItoIntegralCLM.simpleAssembly_T_denseRange' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralCLM.simpleAssembly_T_denseRange /-- info: 'MathFin.ItoIntegralCLM.itoIntegralCLM_T_norm' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralCLM.itoIntegralCLM_T_norm /-! ## Unbounded-horizon `[0,∞)` Itô integral CLM (Summit B / B2) -/ /-- info: 'MathFin.ItoIntegralL2.itoIntegralL2_norm' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralL2.itoIntegralL2_norm /-! ## Process-level elementary Itô integral `t ↦ (V●B)_t` — genuine `L²` content -/ /-- info: 'MathFin.ItoIntegralProcess.memLp_itoSimpleProcess' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcess.memLp_itoSimpleProcess /-- info: 'MathFin.ItoIntegralProcess.itoSimpleProcess_eq_itoSimple' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcess.itoSimpleProcess_eq_itoSimple /-! ## Keystone `∫₀ᵀ B dB = ½(B_T² − B₀² − T)` through the CLM (its first genuine consumer) -/ /-- info: 'MathFin.ItoIntegralBrownian.itoIntegralCLM_T_brownian' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralBrownian.itoIntegralCLM_T_brownian /-! ## Discrete squaring identity (the pathwise Itô keystone) -/ /-- info: 'MathFin.discrete_squaring_identity' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.discrete_squaring_identity /-! ## Itô's lemma for f(x) = x² — the L² continuous form (the QF-keystone) -/ /-- info: 'MathFin.itoSquared_L2_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.itoSquared_L2_tendsto /-- info: 'MathFin.itoSquared_L2_tendsto_div2' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.itoSquared_L2_tendsto_div2 /-! ## Itô chain items 3-6: polynomial remainders, 2D Itô, GBM-SDE, BS-PDE -/ /-- info: 'MathFin.discrete_cubing_identity' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.discrete_cubing_identity /-- info: 'MathFin.discrete_ito_formula_2d' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.discrete_ito_formula_2d /-- info: 'MathFin.hasDerivAt_gbmValue_space' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.hasDerivAt_gbmValue_space /-- info: 'MathFin.gbm_solves_sde' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.gbm_solves_sde /-- info: 'MathFin.bs_pde_eq_itoDrift2D_minus_rV' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.bs_pde_eq_itoDrift2D_minus_rV /-! ## Margrabe BSCallHyp grounding (leap-3 closure via gaussian vector) -/ /-- info: 'MathFin.normalizedSpread_hasLaw_std' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.normalizedSpread_hasLaw_std /-- info: 'MathFin.margrabe_bsCallHyp_of_gaussian' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.margrabe_bsCallHyp_of_gaussian /-- info: 'MathFin.margrabe_price_of_gaussian' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.margrabe_price_of_gaussian /-! ## Portfolio / risk / performance -/ /-- info: 'MathFin.portfolioVarTwo_ge_min' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.portfolioVarTwo_ge_min /-- info: 'MathFin.gaussianVaR_translation' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.gaussianVaR_translation /-- info: 'MathFin.gaussianCVaR_sub_VaR' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.gaussianCVaR_sub_VaR /-- info: 'MathFin.sharpeRatio_affine_invariant' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms MathFin.sharpeRatio_affine_invariant /-! ## Certified cross-domain bridges -/ /-- info: 'MathFin.portfolioVarN_diag_eq_herfindahl' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.portfolioVarN_diag_eq_herfindahl /-- info: 'MathFin.survivalFromForce_eq_hazardSurvival' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.survivalFromForce_eq_hazardSurvival /-- info: 'MathFin.gompertz_cumHazard' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.gompertz_cumHazard /-! ## CRR → Black–Scholes characteristic-function convergence (the distributional CLT heart) -/ /-- info: 'MathFin.crr_charFun_pow_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.crr_charFun_pow_tendsto /-- info: 'MathFin.crr_charFun_pow_tendsto_gaussian' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.crr_charFun_pow_tendsto_gaussian /-- info: 'MathFin.crr_tendsto_gaussian_inDistribution' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.crr_tendsto_gaussian_inDistribution /-! ## Continuous-time first FTAP (discounted GBM price is a Q-martingale) -/ /-- info: 'MathFin.discountedGBM_isMartingale' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.discountedGBM_isMartingale /-! ## Binomial pricing as discounted risk-neutral expectation (CRR→BS price bridge) -/ /-- info: 'MathFin.binomialPrice_eq_integral_convPow' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.binomialPrice_eq_integral_convPow /-! ## CRR → Black–Scholes call-price convergence (the named theorem) -/ /-- info: 'MathFin.binomialPrice_call_tendsto_bs' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.binomialPrice_call_tendsto_bs /-! ## CRR → Black–Scholes call price in literal closed form `S₀Φ(d₁) − Ke^{−rT}Φ(d₂)` -/ /-- info: 'MathFin.binomialPrice_call_tendsto_bs_closed' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.binomialPrice_call_tendsto_bs_closed /-! ## Summit A: bounded-derivative continuous-time Itô formula in L² (CLM-identified) -/ /-- info: 'MathFin.tendsto_weighted_qv' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.tendsto_weighted_qv /-- info: 'MathFin.tendsto_ito_remainder' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.tendsto_ito_remainder /-- info: 'MathFin.ItoIntegralRiemannBridge.itoIntegralCLM_T_of_bdd_cont' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralRiemannBridge.itoIntegralCLM_T_of_bdd_cont /-- info: 'MathFin.ito_formula_L2_bddDeriv' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ito_formula_L2_bddDeriv /-! ## Summit A′: time-dependent Itô formula in L² (CLM-identified) -/ /-- info: 'MathFin.tendsto_weighted_qv_process' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.tendsto_weighted_qv_process /-- info: 'MathFin.tendsto_ito_remainder_td' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.tendsto_ito_remainder_td /-- info: 'MathFin.ItoIntegralRiemannBridgeTD.itoIntegralCLM_T_of_bdd_cont_td' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralRiemannBridgeTD.itoIntegralCLM_T_of_bdd_cont_td /-- info: 'MathFin.ito_formula_td_L2_bddDeriv' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ito_formula_td_L2_bddDeriv /-! ## Localized (exponential-growth) time-dependent Itô formula — the rung-3 unlock to GBM -/ /-- info: 'MathFin.pathIntegral_expGrowth_memLp' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.pathIntegral_expGrowth_memLp /-- info: 'MathFin.ito_formula_td_localized' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ito_formula_td_localized /-! ## Itô → pricing bridge: geometric Brownian motion decomposed by the Itô integral `ItoFormulaGBM.lean`: the **first pricing-ward consumer of the analytic Itô tower** (which until now had none — GBM/BS pricing ran via separate algebraic towers and the Wald exponential). The localized formula, applied to the *time-localized* GBM exponent `(t,x) ↦ S₀ exp((m−σ²/2)·φₙ(t) + σx)` (identity on `[0,T]`, globally bounded so the exp-growth hypotheses hold uniformly in time), yields `ito_formula_gbm`: `Ŝ(T) − Ŝ(0) =ᵐ itoIntegralCLM_T gfx + ∫₀ᵀ m·Ŝ ds`. Setting `m = 0` (`discountedGBM_eq_itoIntegral`) makes the drift vanish — the Itô-integral content of the discounted-GBM martingale, grounding it on the continuous Itô integral rather than the Wald exponential. -/ /-- info: 'MathFin.ito_formula_gbm' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ito_formula_gbm /-- info: 'MathFin.discountedGBM_eq_itoIntegral' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.discountedGBM_eq_itoIntegral /-! ## Itô formula against a constant-coefficient Itô process `ItoFormulaItoProcess.lean`: generalizes the GBM decomposition from the exponential value function to an arbitrary `C³` exponential-growth `f`. For `X_t = X₀ + b·t + σ B_t`, `ito_formula_itoProcess` gives `f(X_T) − f(X₀) =ᵐ itoIntegralCLM_T gfx + ∫₀ᵀ (f'(X)·b + ½f''(X)·σ²) ds` — i.e. `∫ f'(X) dX + ½∫ f''(X)σ² ds`, the diffusion the genuine Itô integral. Same time-localization of the `b·t` exponent as the GBM case; constant coefficients keep the diffusion integrand a function of `B`. -/ /-- info: 'MathFin.ito_formula_itoProcess' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ito_formula_itoProcess /-! ## The time-dependent Itô formula as a process (semimartingale decomposition) `ItoFormulaProcess.lean`: lifts the terminal Itô formula (a single fixed-horizon `Lp` statement) to a process identity holding for **every** `t ≤ T`: `f(t,B_t) − f(0,B_0) =ᵐ itoProcessL2Inf t F + ∫₀ᵗ (f_t + ½f_xx) ds`, the stochastic term the genuine Itô-integral *process* — a continuous `L²` martingale with an everywhere-continuous local-martingale modification. The witness is canonical (`ito_formula_td_L2_bddDeriv` exposes `gfx =ᵐ [f_x(·,B)]`); the construction is the zero-extension `exists_fullHorizon_extension` fed to the existing `[0,∞)` horizon-consistency. No Markov property, no PDE — entirely inside the Itô tower. -/ /-- info: 'MathFin.ito_formula_td_process' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ito_formula_td_process /-! ## Carr–Madan static replication / spanning formula -/ /-- info: 'MathFin.carrMadan_spanning' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.carrMadan_spanning /-- info: 'MathFin.carrMadan_log_spanning' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.carrMadan_log_spanning /-! ## Binomial martingale representation (market completeness) -/ /-- info: 'MathFin.binomial_martingale_representation' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.binomial_martingale_representation /-! ## Path-1 upgrades (2026-06-04): reduced cores earned to full derivations -/ /-- info: 'MathFin.submartingale_optional_sampling' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.submartingale_optional_sampling /-- info: 'MathFin.portfolioVarN_covariance_eq_variance' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.portfolioVarN_covariance_eq_variance /-- info: 'MathFin.gaussianCVaR_isLeast_ruObjective' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.gaussianCVaR_isLeast_ruObjective /-- info: 'MathFin.survival_probability_eq_Phi_distanceToDefault' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.survival_probability_eq_Phi_distanceToDefault /-- info: 'MathFin.newtonStep_quadratic_error' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.newtonStep_quadratic_error /-- info: 'MathFin.newtonSeq_tendsto_root' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.newtonSeq_tendsto_root /-- info: 'MathFin.snellAux_le_of_supermartingale_of_ge' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.snellAux_le_of_supermartingale_of_ge /-- info: 'MathFin.snellAux_eq_discounted_americanPrice' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.snellAux_eq_discounted_americanPrice /-- info: 'MathFin.discounted_americanPrice_supermartingale' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.discounted_americanPrice_supermartingale /-- info: 'MathFin.discounted_intrinsic_le_americanPrice' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.discounted_intrinsic_le_americanPrice -- Poisson-process theory + Itô-process QV (2026-06-05 full-push round) /-- info: 'MathFin.PoissonSuperposition.poissonMeasure_conv_poissonMeasure' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.PoissonSuperposition.poissonMeasure_conv_poissonMeasure /-- info: 'MathFin.PoissonSuperposition.indepFun_map_add_poissonMeasure' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.PoissonSuperposition.indepFun_map_add_poissonMeasure /-- info: 'MathFin.PoissonThinning.markedPoissonMeasure_eq_prod' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.PoissonThinning.markedPoissonMeasure_eq_prod /-- info: 'MathFin.PoissonThinning.thinned_streams' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.PoissonThinning.thinned_streams /-- info: 'MathFin.PoissonCounting.map_count_eq_poissonMeasure' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.PoissonCounting.map_count_eq_poissonMeasure /-- info: 'MathFin.PoissonInterarrival.map_firstArrival_eq_expMeasure' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.PoissonInterarrival.map_firstArrival_eq_expMeasure /-- info: 'MathFin.PoissonInterarrival.survival_factorizes' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.PoissonInterarrival.survival_factorizes /-- info: 'MathFin.ItoProcessQV.tendsto_qv_ito_process' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoProcessQV.tendsto_qv_ito_process -- Finance layer over the Poisson/QV track (2026-06-06): variance-swap drift -- immunity, first-to-default additivity, Poisson pgf, Merton jump-diffusion /-- info: 'MathFin.tendsto_realizedVariance_gbm_L2' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.tendsto_realizedVariance_gbm_L2 /-- info: 'MathFin.firstToDefault_spread_eq_sum_hazards' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.firstToDefault_spread_eq_sum_hazards /-- info: 'MathFin.PoissonPgf.integral_pow_poissonMeasure' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.PoissonPgf.integral_pow_poissonMeasure /-- info: 'MathFin.mertonCallTerm_eq_integral' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.mertonCallTerm_eq_integral /-- info: 'MathFin.integral_mertonSpot' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.integral_mertonSpot /-- info: 'MathFin.merton_put_call_parity' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.merton_put_call_parity -- Merton dominance + classic display; Markov path law (2026-06-06): jump -- risk is never free (spot convexity + compensation identity), the -- Λ′ = Λ(1+k) textbook display (rate-shift identity), and Saporito 1.1.2 -- derived from the pin's Ionescu–Tulcea trajectory kernels /-- info: 'MathFin.bsV_spot_convexOn' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.bsV_spot_convexOn /-- info: 'MathFin.bsV_le_mertonCallPrice' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.bsV_le_mertonCallPrice /-- info: 'MathFin.mertonCallPrice_eq_classic_tsum' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.mertonCallPrice_eq_classic_tsum /-- info: 'MathFin.markovPathMeasure_cylinder' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.markovPathMeasure_cylinder -- Blueprint-spine closure (2026-06-06): every spine node is axiom-pinned. -- Gap found by tests/test_values.py::test_blueprint_spine_is_audited on its -- first run — seven tagged headliners (including bs_identity, the magic -- identity itself) had no guard. /-- info: 'MathFin.WienerIntegralL2.wiener_assembly_isometry' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.WienerIntegralL2.wiener_assembly_isometry /-- info: 'MathFin.ItoIntegralCLM.itoIntegralCLM_T' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralCLM.itoIntegralCLM_T /-- info: 'MathFin.discrete_ito_formula' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.discrete_ito_formula /-- info: 'MathFin.hasLaw_esscher_tilt' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.hasLaw_esscher_tilt /-- info: 'MathFin.BSCallHyp.of_isPreBrownian' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.BSCallHyp.of_isPreBrownian /-- info: 'MathFin.bs_identity' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.bs_identity /-- info: 'MathFin.bs_pde_from_no_arbitrage' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.bs_pde_from_no_arbitrage -- Values round 6 (2026-06-09): Andre's reflection-principle counting -- bijection (Binomial/PathReflection.lean), wired to the corpus as -- `mf-reflection-principle-counting`. /-- info: 'MathFin.reflectionPrincipleEquiv_below' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.reflectionPrincipleEquiv_below -- Summit B / B1a (2026-06-10): the elementary Itô integral, viewed as a process -- `t ↦ (V●B)_t`, is an adapted L² martingale -- (Foundations/ItoIntegralProcessMartingale.lean). Infrastructure for the -- gated Girsanov/Lévy/martingale-representation/SDE cluster; no corpus entry -- yet (the `full` entry lands with B1b, the general integrand). /-- info: 'MathFin.ItoIntegralProcess.itoSimpleProcess_adaptedAt' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcess.itoSimpleProcess_adaptedAt /-- info: 'MathFin.ItoIntegralProcess.condExp_adapted_mul_increment' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcess.condExp_adapted_mul_increment /-- info: 'MathFin.ItoIntegralProcess.itoSimpleProcess_isMartingale' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcess.itoSimpleProcess_isMartingale /-- info: 'MathFin.ItoIntegralProcess.itoSimpleProcess_isometry_time' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcess.itoSimpleProcess_isometry_time /-- info: 'MathFin.ItoIntegralProcess.itoSimpleProcessLp_l2_continuous' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcess.itoSimpleProcessLp_l2_continuous -- Summit B / B3 (2026-06-13): the elementary Itô integral as a continuous LOCAL -- MARTINGALE — pathwise continuity (given continuous Brownian paths) + Degenne's -- `Martingale.IsLocalMartingale` (`Foundations/ItoIntegralProcessLocalMartingale.lean`). -- The localization entry point; consumes the upstream local-martingale class. /-- info: 'MathFin.ItoIntegralProcess.itoSimpleProcess_pathContinuous' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcess.itoSimpleProcess_pathContinuous /-- info: 'MathFin.ItoIntegralProcess.itoSimpleProcess_isLocalMartingale' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcess.itoSimpleProcess_isLocalMartingale -- Summit B / B1b (2026-06-12): the GENERAL-integrand Itô integral -- `(φ●B)_t = ∫₀ᵗ φ dB` for `φ ∈ L2Predictable[0,T]`, built by extending B1a's -- t-process along the dense `simpleAssembly_T` (`Foundations/ItoIntegralProcessGeneral.lean`). -- The key identity `(φ●B)_t = E[∫₀ᵀ φ dB | 𝓕_t]` gives the L² martingale property, -- a.e.-adaptedness, the contraction and terminal Itô isometry, and L²-continuity. -- The explicit time-indexed isometry E[(φ●B)_t²] = ∫₀ᵗ E[φ²] ds is deferred. /-- info: 'MathFin.ItoIntegralProcessGeneral.itoProcessCLM_eq_condExpL2' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessGeneral.itoProcessCLM_eq_condExpL2 /-- info: 'MathFin.ItoIntegralProcessGeneral.itoIntegralProcessGen_isMartingale' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessGeneral.itoIntegralProcessGen_isMartingale /-- info: 'MathFin.ItoIntegralProcessGeneral.itoProcessCLM_aeStronglyMeasurable' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessGeneral.itoProcessCLM_aeStronglyMeasurable /-- info: 'MathFin.ItoIntegralProcessGeneral.itoProcessCLM_norm_le' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessGeneral.itoProcessCLM_norm_le /-- info: 'MathFin.ItoIntegralProcessGeneral.itoProcessCLM_norm_terminal' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessGeneral.itoProcessCLM_norm_terminal /-- info: 'MathFin.ItoIntegralProcessGeneral.itoIntegralProcessGen_l2_continuous' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessGeneral.itoIntegralProcessGen_l2_continuous -- The deferred per-`t` Itô isometry `E[(φ●B)_t²] = ∫_{(0,t]×Ω} φ²` -- (`Foundations/ItoIntegralProcessIsometry.lean`), proved by density-transferring the -- band-restricted simple-process isometry against the band-truncation CLM. /-- info: 'MathFin.ItoIntegralProcessGeneral.itoProcessCLM_norm_sq' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessGeneral.itoProcessCLM_norm_sq -- Covariation of Itô integrals (2026-06-23): the BILINEAR Itô isometry. The Itô -- integral, bundled as a `LinearIsometry` (`itoIsometry_T`), preserves the -- L²-inner product (`LinearIsometry.inner_map_map`, polarization of the norm -- isometry), giving `𝔼[(∫φ dB)(∫ψ dB)] = ⟪φ, ψ⟫` and, on the diagonal, the Itô -- isometry itself (`Foundations/ItoIntegralCovariation.lean`). The bilinear -- completion of B1 and the covariance backbone for covariance-swap pricing. /-- info: 'MathFin.ItoIntegralCovariation.itoIsometry_T' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralCovariation.itoIsometry_T /-- info: 'MathFin.ItoIntegralCovariation.inner_itoIntegralCLM_T' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralCovariation.inner_itoIntegralCLM_T /-- info: 'MathFin.ItoIntegralCovariation.covariation_itoIntegralCLM_T' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralCovariation.covariation_itoIntegralCLM_T /-- info: 'MathFin.ItoIntegralCovariation.variance_itoIntegralCLM_T' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralCovariation.variance_itoIntegralCLM_T -- Continuous modification of the general-integrand Itô process (2026-06-26): the -- first PATHWISE-regularity result for the general integrand and the tower→pricing -- gate. Simple approximants `Vₙ ● B` (B3-continuous) are a.s.-uniformly Cauchy on -- `[0,T]` (Doob's continuous-time maximal inequality + Borel–Cantelli on a fast -- subsequence), so their uniform limit `itoContinuousMod` is pathwise continuous, -- equals the L² process `itoProcessCLM T t φ` a.e. at every `t ≤ T` (a modification, -- via `tendstoInMeasure_ae_unique`), and is bundled by `exists_continuous_modification_itoProcess` -- (`Foundations/ItoIntegralProcessContinuousModification.lean`). Non-redundant: Degenne's -- general càdlàg modification is `sorry`-backed, and this L²+Doob route yields a -- genuinely continuous (not merely càdlàg) version. /-- info: 'MathFin.ItoIntegralProcessContinuousModification.itoContinuousMod_modification' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessContinuousModification.itoContinuousMod_modification /-- info: 'MathFin.ItoIntegralProcessContinuousModification.itoContinuousMod_continuousOn' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessContinuousModification.itoContinuousMod_continuousOn /-- info: 'MathFin.ItoIntegralProcessContinuousModification.exists_continuous_modification_itoProcess' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessContinuousModification.exists_continuous_modification_itoProcess -- The IsLocalMartingale follow-on (`Foundations/ItoIntegralProcessLocalMartingaleGeneral.lean`): -- the everywhere-continuous representative of the modification, adapted to the -- NULL-AUGMENTED Brownian filtration `𝓕ᴮ ⊔ 𝓝`, is a genuine `IsLocalMartingale`. -- The measure-theoretic heart is `condExp_sup_nulls` — conditioning on the null -- augmentation agrees a.e. with conditioning on `𝓕ᴮ` (proved via the σ-algebra crux -- `exists_ae_eq_of_sup_nulls`), which transfers the L² martingale property to the -- a.e.-defined modification while repairing it into an everywhere-continuous adapted -- process — the `∀ ω, IsCadlag` hypothesis of Degenne's `Martingale.IsLocalMartingale`. /-- info: 'MathFin.ItoIntegralProcessLocalMartingaleGeneral.exists_continuous_localMartingale_modification' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessLocalMartingaleGeneral.exists_continuous_localMartingale_modification -- The [0,∞) crown (`Foundations/ItoIntegralProcessLocalMartingaleInfinite.lean`): the per-horizon -- continuous local martingales are glued — horizon consistency (`itoProcessL2Inf_eq_itoProcessCLM`, -- itself resting on the `[0,T]` `SimpleProcess` clamp) makes each a modification of the SAME -- unbounded-horizon process, and `indistinguishable_of_modification_on` agrees them on overlaps — -- into a single everywhere-continuous local martingale on the WHOLE half-line, whose martingale -- property is the GLOBAL `itoProcessL2Inf_isMartingale` through `condExp_sup_nulls` (no horizon clamp). /-- info: 'MathFin.ItoLocalMartingaleInfinite.exists_continuous_localMartingale_modification_infinite' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoLocalMartingaleInfinite.exists_continuous_localMartingale_modification_infinite /-! ## Finite-Ω Fundamental Theorem of Asset Pricing (Harrison–Pliska, 2026-06-25) -/ -- The separating-dual kernel (`Foundations/ConvexSeparation.lean`): a finite-dim -- subspace disjoint from the standard simplex admits a strictly-positive -- annihilating dual (finite-dimensional geometric Hahn–Banach). The geometric -- core shared by the single- and multi-period FTAP backward directions. /-- info: 'MathFin.exists_pos_dual_of_disjoint_stdSimplex' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.exists_pos_dual_of_disjoint_stdSimplex -- The cone-separation root (`Foundations/ConvexDuality.lean`): a closed convex -- CONE disjoint from the standard simplex admits a strictly-positive functional -- that is `≤ 0` on the cone (finite-dimensional geometric Hahn–Banach). Generalizes -- the separating-dual kernel from a subspace (two-sided `= 0`) to a cone (one-sided -- `≤ 0`); the geometric heart shared by the FTAP gains cone, the coherent-risk -- acceptance cone, and the superhedging super-replication cone. /-- info: 'MathFin.exists_pos_separating_of_cone_disjoint_simplex' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.exists_pos_separating_of_cone_disjoint_simplex /-- info: 'MathFin.exists_separating_of_not_mem_cone' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.exists_separating_of_not_mem_cone /-- info: 'MathFin.coherentRisk_isLUB' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.coherentRisk_isLUB /-- info: 'MathFin.worstCase_isLUB' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.worstCase_isLUB /-- info: 'MathFin.emm_le_superReplication' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.emm_le_superReplication -- The Bayes change-of-measure engine (`Foundations/ChangeOfMeasure.lean`): `Z` and -- `Z·D` both `P`-martingales ⇒ `D` is a `Q`-martingale on `[0,T]` for `Q = withDensity Z_T`. -- The abstract kernel of Girsanov, no stochastic calculus — only conditional expectations. /-- info: 'MathFin.changeOfMeasure_setIntegral_eq' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.changeOfMeasure_setIntegral_eq -- Black–Scholes EMM via Girsanov (`Foundations/Girsanov.lean`): the discounted stock is a -- martingale under the tilted measure `Q = withDensity(exp(−θX_T − ½θ²T))` — the risk-neutral -- measure as an explicit change of measure, retiring the Wald shortcut. Consumes the engine. /-- info: 'MathFin.bs_discounted_isQMartingale' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.bs_discounted_isQMartingale -- Multi-state single-period FTAP, now a biconditional (`FTAPMultiState.lean`): -- the backward direction (no arbitrage ⟹ EMM) via the separating-dual kernel. /-- info: 'MathFin.hasEMM_multi_iff_not_hasArbitrage' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.hasEMM_multi_iff_not_hasArbitrage -- Finite-Ω multi-period FTAP (`FTAPDiscrete.lean`): NoArbitrage ⟺ ∃ EMM, the -- finite case of Dalang–Morton–Willinger. Backward via global separation of the -- attainable-gains subspace from the simplex; forward via transform telescoping. /-- info: 'MathFin.ftap_discrete' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ftap_discrete -- General-Ω one-period FTAP (`FTAPOnePeriod.lean`): NoArbitrage ⟺ ∃ EMM for a -- scalar L⁰ return on an arbitrary probability space (Föllmer–Schied 1.55 / -- one-period DMW). Backward via the bounded-density reduction to L¹, the scalar -- no-arbitrage dichotomy, and the two-region balancing `withDensity` — no -- Hahn–Banach, no Kreps–Yan. /-- info: 'MathFin.OnePeriod.ftap_one_period' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.OnePeriod.ftap_one_period -- General-Ω one-period FTAP, d assets (`FTAPOnePeriodVector.lean`): NoArbitrage ⟺ ∃ EMM -- for a non-redundant ℝᵈ-valued L⁰ return on an arbitrary probability space. Backward via -- the explicit Esscher / minimal-divergence density z = σ⟪θ₀,Y⟫ minimising the softplus -- potential — no Hahn–Banach, no L⁰-cone closedness, no measurable selection. /-- info: 'MathFin.OnePeriodVector.ftap_one_period_vector' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.OnePeriodVector.ftap_one_period_vector /-! ## Itô → pricing bridge: the deterministic-integrand Wiener integral is Gaussian `WienerIntegralGaussian.lean`: a deterministic-integrand Itô integral `∫ f dB` is `gaussianReal 0 ‖f‖²` (charFun route: simple-process Gaussianity + density + Lévy / `Measure.ext_of_charFun`). Its first pricing consumer is the Vasicek terminal law (`VasicekSDEGaussian.lean`): the SDE solution `r_T = mean + σ ∫₀ᵀ e^{−κ(T−s)} dB_s` has the posited law `N(mean, σ²(1−e^{−2κT})/(2κ))`, **derived** rather than assumed — the first Itô-tower consumer in FixedIncome. -/ /-- info: 'MathFin.WienerIntegralL2.wienerIntegralLp_map_eq_gaussianReal' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.WienerIntegralL2.wienerIntegralLp_map_eq_gaussianReal /-- info: 'MathFin.vasicekShortRate_hasLaw_gaussian' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.vasicekShortRate_hasLaw_gaussian /-! ## The Brownian exit times as a localizing sequence — the localization engine `ExitTime.lean`: the exit times `τ_N = inf {t : N ≤ |B_t|}` of the closed exterior form the repo's first genuine `IsLocalizingSequence` (`isLocalizingSequence_exitTime`). Each `τ_N` is a stopping time for the **raw** Brownian filtration (`isStoppingTime_exitTime`) — the closed exterior makes `{τ_N ≤ i}` the attained-`sInf` event, a rational `⋂ₘ⋃_{q≤i}` measurable in `𝓕_i` with **no right-continuity** (the open-exterior route would need `𝓕_{i⁺}`, i.e. Blumenthal). Monotone in `N` and escaping to `⊤` a.s. (continuous paths bounded on compacts), it is the localization machinery that lifts the bounded-derivative Itô formula toward unbounded coefficients (Summit C). -/ /-- info: 'MathFin.isStoppingTime_exitTime' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.isStoppingTime_exitTime /-- info: 'MathFin.isLocalizingSequence_exitTime' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.isLocalizingSequence_exitTime /-! ## The unrestricted-`C³` Itô formula via stopping-time localization (Summit C) `ItoFormulaUnrestricted.lean`: for a general `C³` `f` (six partials, all jointly continuous, **no** growth or boundedness hypothesis), the compensated process `M_t = f(t,B_t) − f(0,B_0) − ∫₀ᵗ drift` is everywhere-continuous, satisfies the Itô identity by construction, and is a **continuous local martingale in explicit form** (`ito_formula_unrestricted_local`): a localizing sequence `σ_N = min(τ_N, N) ↑ ⊤` plus per-`N` continuous **true** martingales `Mₙ` agreeing with `M` on the stochastic interval `{t ≤ σ_N}`. The engine is the double cutoff `f(φₙ·, φₙ·)` (time *and* space), whose globally-bounded derivatives let `ito_formula_td_process` apply; the cuts are inert on `{t ≤ σ_N}`, where `Mₙ` agrees with `M`. The all-time agreement `indistinguishable_on_stochInterval` lifts the per-`t` agreement to the whole stochastic interval (dense rationals + continuity). -/ /-- info: 'MathFin.ito_formula_unrestricted_local' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ito_formula_unrestricted_local /-- info: 'MathFin.indistinguishable_on_stochInterval' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.indistinguishable_on_stochInterval /-! ## Summit C in Degenne's `IsLocalMartingale` typeclass `ItoFormulaUnrestrictedLocMart.lean`: the unrestricted-`C³` residual `M` is a genuine `IsLocalMartingale` on the null-augmented Brownian filtration (`ito_formula_unrestricted`). The one ingredient beyond the explicit form is the **adaptedness** of `M` (`residual_stronglyMeasurable`), i.e. of the drift primitive `D_t = ∫₀ᵗ drift` (`driftPrimitive_stronglyMeasurable`): time-clamping the integrand makes every slice `𝓕_t`-measurable, so it is jointly strongly measurable (Carathéodory) and the integral is `𝓕_t`-measurable (`StronglyMeasurable.integral_prod_right`). With `M` adapted, `StronglyAdapted.stoppedProcess_indicator` + the all-time agreement assemble `Locally (Martingale ∧ cadlag)` with the exit-time localizer `σ_N`. -/ /-- info: 'MathFin.ito_formula_unrestricted' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ito_formula_unrestricted /-! ## SDE existence & uniqueness — the Picard fixed point (#44) The strong solution of `dX = b(X)dt + σ(X)dB` is the unique fixed point of the Picard iterate `Φ(X) = η + ∫₀ᵗ b(X)ds + ∫₀ᵗ σ(X)dB` on the predictable `L²` space `E`. `picardMap_contraction` is the a priori contraction estimate `‖Φ X − Φ Y‖ ≤ (T·L_b + √T·L_σ)·‖X − Y‖` (drift operator norm `T` × Cauchy–Schwarz, Itô operator norm `√T` × isometry); `picardMap_exists_unique_fixedPoint` obtains existence and uniqueness via Banach's theorem. Both stand on the assembled Itô/drift operators. -/ /-- info: 'MathFin.SDEExistence.picardMap_contraction' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.SDEExistence.picardMap_contraction /-- info: 'MathFin.SDEExistence.picardMap_exists_unique_fixedPoint' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.SDEExistence.picardMap_exists_unique_fixedPoint /-! ## SDE strong-solution uniqueness — the L²-energy Grönwall argument (#19) The uniqueness half of Theorem 8.2.5, now a genuinely *derived* theorem rather than an assumed field. `gronwall_zero_of_le_const_mul_integral` is the reusable integral Grönwall (`g ≥ 0`, `g t ≤ K·∫₀ᵗ g` on `[0,b]` ⟹ `g ≡ 0`), obtained from Mathlib's differential `eq_zero_of_abs_deriv_le_mul_abs_self_of_eq_zero_right` fed the primitive `G t = ∫₀ᵗ g` (FTC). `sde_pathwise_uniqueness` runs the `L²`-energy method: `E t = 𝔼[(Xₜ−Yₜ)²]` satisfies `E t ≤ (2·Cdrift·t + 2·Cdiff)·∫₀ᵗ E` and Grönwall forces `E ≡ 0`. `IsL2SolutionPair.uniqueness` is the packaged Theorem 8.2.5 (uniqueness): the drift energy bound is *derived* from Lipschitz `μ` (via `drift_energy_le`, Cauchy–Schwarz + Tonelli), the diffusion from the Itô isometry field. -/ /-- info: 'MathFin.gronwall_zero_of_le_const_mul_integral' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.gronwall_zero_of_le_const_mul_integral /-- info: 'MathFin.sde_pathwise_uniqueness' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.sde_pathwise_uniqueness /-- info: 'MathFin.IsL2SolutionPair.uniqueness' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.IsL2SolutionPair.uniqueness /-! ## SDE pathwise existence — the E-fixed point as a sample-path process (#19 → existence bridge) `SDEExistence` produced the strong solution as the abstract `L²` fixed point `picardSolution ∈ E`; this bridge realizes it as a genuine *pathwise* process. `driftContinuousMod_tendsto` is the drift analog of `itoContinuousMod_tendsto`: the elementary drifts `∫₀ᵗ Vₙ ds` converge a.e. — via a direct Chebyshev maximal bound (no martingale, unlike the Itô side's Doob inequality) plus Borel–Cantelli. `driftProcessAssembled_coeFn` is the crux: the abstract `extendOfNorm` drift operator's `coeFn` equals that pointwise `limUnder` a.e. — two convergences of `driftSimpleProcessLp Vₙ` (CLM-continuity to the operator, and a.e. to the pathwise limit, the latter lifted from per-slice to the trim measure through the predictable-measurable convergence set) are unique in measure on the finite trim space. `sde_pathwise_decomposition` slices the fixed-point equation `X = Φ(X)` into the sample-path identity `X_t(ω) = η(ω) + driftContinuousMod(b∘X)_t(ω) + itoContinuousMod(σ∘X)_t(ω)`. -/ /-- info: 'MathFin.ItoIntegralProcessContinuousModification.driftContinuousMod_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessContinuousModification.driftContinuousMod_tendsto /-- info: 'MathFin.ItoIntegralProcessContinuousModification.driftProcessAssembled_coeFn' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessContinuousModification.driftProcessAssembled_coeFn /-- info: 'MathFin.SDEExistence.sde_pathwise_decomposition' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.SDEExistence.sde_pathwise_decomposition /-! ## SDE pathwise drift — the honest single Lebesgue integral (#33) The drift term of the pathwise solution, refined from the abstract `limUnder` to the recognizable integral. `driftContinuousMod_eq_setIntegral` proves `driftContinuousMod g t ω = ∫₀ᵗ ⇑g(s,ω) ds` a.e. for every `t ≤ T`: the elementary drifts `∫₀ᵗ Vₙ ds` converge to `driftContinuousMod` (Layer 2), and the ω-slice energies `Dₙ(ω) = ∫₀ᵀ(⇑Vₙ − ⇑g)² ds` decay in `L¹(μ)` (`= ‖simpleAssembly_T Vₙ − g‖²`, `drift_slice_energy_eq`, Tonelli through the trim↔product transfer), so a subsequence has `Dₙₖ(ω) → 0` a.e., whence the interval Cauchy–Schwarz `|∫₀ᵗ(⇑Vₙₖ − ⇑g)| ≤ √(T·Dₙₖ(ω)) → 0` matches the limits. `sde_pathwise_drift_eq_setIntegral` specializes it to `b∘X`, giving the strong solution's drift as `∫₀ᵗ b(X_s(ω)) ds`. -/ /-- info: 'MathFin.ItoIntegralProcessContinuousModification.drift_slice_energy_eq' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessContinuousModification.drift_slice_energy_eq /-- info: 'MathFin.ItoIntegralProcessContinuousModification.driftContinuousMod_eq_setIntegral' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessContinuousModification.driftContinuousMod_eq_setIntegral /-- info: 'MathFin.SDEExistence.sde_pathwise_drift_eq_setIntegral' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.SDEExistence.sde_pathwise_drift_eq_setIntegral /-! ## The change of numéraire — price invariance (IV↔I seam) The numéraire measure `Q^N = Q.withDensity((N_T·B₀)/(N₀·B_T))` reprices every terminal claim consistently: `changeOfNumeraire` is the invariance `N₀·𝔼^{Q^N}[X/N_T] = B₀·𝔼^Q[X/B_T]`, a pure measure-transport identity plus cancellation of `N_T` — no integrability hypothesis. `numeraireMeasure_isProbabilityMeasure` is the companion normalization (`N/B` a `Q`-martingale ⟹ `Q^N` a probability measure). The abstract backbone is genuinely CONSUMED: `stockNumeraireMeasure_eq_numeraireMeasure` exhibits the Black–Scholes stock numéraire `dQ^(S)/dQ = e^{−rT}·S_T/S₀` as the instance `B_T = e^{rT}`, `B₀ = 1`, `N = S`. -/ /-- info: 'MathFin.changeOfNumeraire' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.changeOfNumeraire /-- info: 'MathFin.numeraireMeasure_isProbabilityMeasure' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.numeraireMeasure_isProbabilityMeasure /-- info: 'MathFin.stockNumeraireMeasure_eq_numeraireMeasure' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.stockNumeraireMeasure_eq_numeraireMeasure /-! ## Two further numéraire seams: the Kelly portfolio ⟹ EMM, and the exchange option `kellyNumeraire_isRiskNeutral` is the discrete numéraire-*portfolio* ⟹ EMM identity: the growth-optimal (Kelly) wealth, used as deflator, turns the physical measure into the risk-neutral one (`q₊·b + q₋·(−1) = 0`), the `p`-independence being the Kelly first-order condition. `exchangeOption_numeraire_price` exhibits Margrabe's `S²`-numéraire valuation as a genuine `changeOfNumeraire` instance (`X` = the exchange payoff, `N = S²`). -/ /-- info: 'MathFin.kellyNumeraire_isRiskNeutral' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.kellyNumeraire_isRiskNeutral /-- info: 'MathFin.exchangeOption_numeraire_price' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.exchangeOption_numeraire_price /-! ## Distributional Girsanov (Track-α): `B^θ` is a `Q`-Brownian motion — constant → simple → continuous adapted (2026-07-09) The three defining Brownian properties of the drift-corrected process — zero start, Gaussian `𝒩(0,t−s)` increments, and independence of disjoint increments — are read off, under the Girsanov measure `Q = P.withDensity(Z_T)`, from a *single* structural hypothesis: that every `exp(a·B^θ − ½a²·)` is a `Q`-martingale on `[0,T]`. That reduction is `isQBrownianMotion_of_expMartingale`, which runs the characteristic-function chain (marginal MGF → increment MGF → joint MGF → linear-combination Gaussian law → independence via `charFun`) exactly ONCE, process-agnostically. Each θ regime then supplies only its own exponential-martingale identity and lands as a one-line application: * `Btheta_isQBrownianMotion` — CONSTANT θ, `Z·D = Wald(a−θ)` a genuine martingale everywhere (the instance that first validated the abstraction against a known-good result). * `Btheta_simple_isQBrownianMotion` — SIMPLE (piecewise-constant adapted) θ, via the spine `E^{−c}·exp(a·B^θ − ½a²·) =ᵐ E^{a−c}` fed to the Bayes change-of-measure engine with an `L²`-Hölder mixed-time integrability. Strictly beyond constant θ, on the existing tower. * `Btheta_isQBrownianMotion_adapted` — the culmination, bounded adapted CONTINUOUS θ under `Z_T = exp(−∫₀ᵀθ dB − ½∫₀ᵀθ² ds)`. **Spine-free**: instead of proving a continuous Doléans stochastic exponential to be a martingale (the Novikov crux), the simple-θ identity is passed to the limit — the mixed-time set-integral `∫_A exp(a·Yⁿ−½)·Zⁿ_T dμ` converges through the a.e.-subsequence engine `tendsto_setIntegral_of_subseq_ae_of_sq_bound` with a route-A L⁴/AM-GM uniform `L²` bound, and no adapted-integrand Itô formula is used anywhere. -/ /-- info: 'MathFin.isQBrownianMotion_of_expMartingale' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.isQBrownianMotion_of_expMartingale /-- info: 'MathFin.Btheta_isQBrownianMotion' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.Btheta_isQBrownianMotion /-- info: 'MathFin.Btheta_simple_isQBrownianMotion' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.Btheta_simple_isQBrownianMotion /-- info: 'MathFin.Btheta_isQBrownianMotion_adapted' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.Btheta_isQBrownianMotion_adapted /-! ### Continuous-time first FTAP: an EMM precludes simple-strategy arbitrage A model-agnostic continuous-market frame (`Foundations/ContinuousMarket.lean`): an **equivalent martingale measure** for a discounted price process precludes arbitrage against **simple** (piecewise-constant, predictable, bounded) strategies — the honest, economically transparent meaning-1 scope (general admissible strategies, NFLVR, and the converse are the deferred Delbaen–Schachermayer meaning-2). The forward theorem is DIRECT: each predictable-weighted increment `⟪φᵢ, S(tᵢ₊₁) − S(tᵢ)⟫` integrates to `0` under `Q` via the bilinear conditional-expectation pull-out (`condExp_bilin_of_stronglyMeasurable_left` with `innerSL ℝ`) and the martingale property, the finite sum vanishes, and the shared closing primitive `ae_zero_of_nonneg_of_integral_zero` — the SAME step the discrete `emm_implies_no_arbitrage` uses, each setting supplying its own zero-integral — finishes. Instantiated at `F = ℝ` by the discounted GBM under its risk-neutral measure (`Q = P`, `discountedGBM_isMartingale` a full-horizon `P`-martingale). -/ /-- info: 'MathFin.ae_zero_of_nonneg_of_integral_zero' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ae_zero_of_nonneg_of_integral_zero /-- info: 'MathFin.ContinuousMarket.isEMM_noArbitrageSimple' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.ContinuousMarket.isEMM_noArbitrageSimple /-- info: 'MathFin.discountedGBM_isEMM' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.discountedGBM_isEMM /-- info: 'MathFin.discountedGBM_noArbitrageSimple' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.discountedGBM_noArbitrageSimple /-! ### Martingale representation, and the completeness it buys The Itô integral `φ ↦ ∫₀ᵀ φ dB` is an isometry (`itoIsometry_T`, audited above); these theorems identify its IMAGE exactly as the centered `𝓕ᴮ_T`-measurable part of `L²(μ)`. Surjectivity of an isometry is a *totality* statement about its range, and it is proved as one: the range is closed (the isometric image of a complete space) hence orthogonally complemented, so a centered `𝓕ᴮ_T`-measurable `F` splits as `y + z` with `z ⊥ range`; `z` inherits measurability and centering, so it is orthogonal to every step-integrand Doléans exponential (`stepDoleans_sub_one_mem_range` puts `D − 1` in the range, centering kills the leftover `1`), and Wiener-exponential totality (`eq_zero_of_orthogonal_stepDoleans`) forces `z = 0`. No Malliavin calculus, no adapted-integrand Itô formula. * `itoIntegralCLM_T_surjective_onto_centered` — submodule form: range ⊔ constants = `lpMeas 𝓕ᴮ_T`. * `exists_itoIntegral_representation` — terminal form, with a UNIQUE integrand (injectivity of an isometry). * `martingale_representation` — process form (corpus `gir-thm-9.3.4`): `M t =ᵐ M 0 + (φ●B)_t` for `t ≤ T`, the terminal integrand spread over the horizon by `itoProcessCLM_eq_condExpL2`. `M 0` is not assumed constant — it is the representation at `t = 0`. The finance reading (`Foundations/MarketCompleteness.lean`) is completeness: `exists_replicating_strategy` hedges every square-integrable `𝓕ᴮ_T`-claim from initial wealth `𝔼_μ[H]`, uniquely. `measure_eq_of_pricesGainsAtZero` is the pricing-measure statement, and its scope is narrower than the textbook second FTAP — deliberately, and the audit records it rather than the slogan. It says: a probability measure `Q ≪ μ` that prices the traded gains at zero agrees with `μ` on all of `𝓕ᴮ_T`. Gains-neutrality is a HYPOTHESIS (`PricesGainsAtZero`), not a consequence of `IsEMM`: the replicating wealth here is an integral against `B`, while an EMM `Q` makes `S` — not `B` — a martingale, and the missing link `∫ φ dS` is absent by design. The hypothesis is guarded by two proved facts, `pricesGainsAtZero_self` (μ satisfies it, so nothing is vacuous) and `pricesGainsAtZero_of_gains_martingale` (the textbook gains-martingale condition implies it). Only `complete ⟹ unique` is delivered; the Jacod–Yor converse is out of scope. -/ /-- info: 'MathFin.itoIntegralCLM_T_surjective_onto_centered' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.itoIntegralCLM_T_surjective_onto_centered /-- info: 'MathFin.exists_itoIntegral_representation' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.exists_itoIntegral_representation /-- info: 'MathFin.martingale_representation' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.martingale_representation /-- info: 'MathFin.exists_replicating_strategy' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.exists_replicating_strategy /-- info: 'MathFin.measure_eq_of_pricesGainsAtZero' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.measure_eq_of_pricesGainsAtZero /-! ### Downside performance metrics (#73) The finite-state Omega identity, finite-path maximum drawdown, and Calmar scaling law are audited here as one public acceptance bundle. -/ /-- info: 'MathFin.downsideMetrics_bundle' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.downsideMetrics_bundle /-! ### von Neumann–Morgenstern expected utility (#178) The layer beneath `RiskMeasures.UtilityDerivation`, which takes the expected-utility form as given: lotteries with their mixture algebra, affinity of the expected-utility functional in the mixture (the pivot — every axiom below is a corollary of it), the vNM axioms verified for the induced preference, and cardinal uniqueness under positive affine rescaling. Soundness half only: the representation theorem (axioms ⟹ ∃u) is deliberately out of scope, and the module doc says so. -/ /-- info: 'MathFin.expectedUtility_mix' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.expectedUtility_mix /-- info: 'MathFin.prefersEU_affine_invariant' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms MathFin.prefersEU_affine_invariant end MathFin.AxiomAudit