/-
Copyright (c) 2026 Raphael Coelho. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Raphael Coelho
-/
module

public import MathFin.Foundations.MartingaleRepresentation
public import MathFin.Foundations.ContinuousMarket

/-!
# Market completeness: replication, superreplication, and the pricing measure

The finance reading of `MartingaleRepresentation`. On the Brownian filtration `𝓕ᴮ`, with `μ` the
measure under which `B` is a Brownian motion — the model's reference measure, which
`measure_eq_of_pricesGainsAtZero` then shows *is* the pricing measure on `𝓕ᴮ_T` — the
representation theorem says exactly that the market driven by `B` is **complete**: every
square-integrable `𝓕ᴮ_T`-claim is the terminal wealth of a strategy started at the claim's
price `𝔼_μ[H]`. Three consequences are recorded here: replication, the superreplication
duality, and uniqueness of the pricing measure.

## The strategy class

Hedges are the **Itô-integrable predictable** integrands `Lp ℝ 2 (trimMeasure_T T)`, the domain
of `itoIntegralCLM_T` — strictly wider than `ContinuousMarket.SimpleStrategy`. The widening is
forced, not chosen: the hedge the representation theorem returns is a general predictable
process, and a general `L²` claim is not the terminal value of any piecewise-constant holding,
so a completeness statement over simple strategies would have no witnesses. `ContinuousMarket`
is untouched; this file is additive.

## `emm_unique_of_complete` — what is proved and what is hypothesised

The textbook second FTAP ("complete ⟹ the martingale measure is unique") runs: for `A ∈ 𝓕_T`
replicate `1_A`; observe that the replicating **wealth process is a stochastic integral against
the price `S`**, hence a martingale under *every* EMM; read off `Q A = V₀`, a number that does
not depend on `Q`.

The middle step is the load-bearing one, and it is unavailable here. The wealth process built by
martingale representation is an integral against `B`, whereas an EMM `Q` for `S` is a measure
under which `S` — not `B` — is a martingale; `S` and `B` share only a filtration. Nothing in
`IsEMM S Q` makes `∫₀ᵀ φ dB` a `Q`-fair game, so the uniqueness statement does **not** follow
from `IsEMM` alone. The missing link is the stochastic integral `∫ φ dS`, whose absence
`ContinuousMarket` already records as deliberate.

The traded-gains condition is therefore hypothesised, under its own name: `PricesGainsAtZero Q`
says every terminal Itô integral is `Q`-integrable with zero `Q`-mean — a fair game for this
strategy class, and precisely what `∫ φ dS` would deliver from `IsEMM`. Two facts keep that
hypothesis honest rather than convenient. It is *satisfied*: `pricesGainsAtZero_self` shows `μ`
itself is such a measure, so nothing here is vacuous. And it is *implied by the textbook
condition*: `pricesGainsAtZero_of_gains_martingale` derives it from a gains process that is a
`Q`-martingale started at `0`.

With it the conclusion is sharper than uniqueness. `measure_eq_of_pricesGainsAtZero` shows every
gains-neutral measure dominated by `μ` agrees with `μ` on `𝓕ᴮ_T` — `μ` *is* the pricing measure
— and `emm_unique_of_complete` is the two-measure corollary landed on `ContinuousMarket.IsEMM`.
Of the four fields of `IsEMM` that corollary consumes `isProb` and `ac`; `martingale` is what
would supply `PricesGainsAtZero` in a theory with `∫ φ dS`, and rides along unused so the
statement stays in the vocabulary a reader looks it up under.

## Scope: one direction only

Only `complete ⟹ unique` is proved. The converse, `unique ⟹ complete`, is the other half of the
second FTAP; it needs the extreme-point characterisation of the set of martingale measures
(Jacod–Yor — the measure is extreme exactly when the stable subspace generated by the price is
dense), and is absent by design in the same sense `ContinuousMarket` records the
Delbaen–Schachermayer boundary: reaching it is additive (a new characterisation of the EMM set),
not a rewrite of what is here.

`superReplication_eq_emm_price` is the **continuous-time** superreplication duality: the least
initial wealth from which some Itô-integrable strategy dominates `H` equals `𝔼_μ[H]`. It does
**not** close the finite-state gap recorded in `Foundations/SuperhedgingDuality`, whose
one-period matrix model proves only the bound `EMM price ≤ superreplication cost`, its reverse
direction needing a Farkas/closedness fact unavailable at this pin. The two equalities hold for
structurally different reasons — separation there, martingale representation here — and neither
implies the other.

## Result

* `Replicates` — the replication predicate: initial wealth plus an Itô integral is the claim.
* `exists_replicating_strategy` — **completeness**: every `L²` `𝓕ᴮ_T`-claim is replicated from
  its price `𝔼_μ[H]`, by a unique hedge.
* `superReplicationPrice` — least initial wealth from which some strategy dominates the claim.
* `superReplication_eq_emm_price` — superreplication duality: that price is `𝔼_μ[H]`.
* `PricesGainsAtZero` — the traded gains are a fair game under `Q`.
* `pricesGainsAtZero_self` — `μ` prices its own traded gains at zero.
* `pricesGainsAtZero_of_gains_martingale` — the textbook hypothesis implies it.
* `integral_eq_of_pricesGainsAtZero` — every such measure prices every replicable claim at
  `𝔼_μ[H]`.
* `measure_eq_of_pricesGainsAtZero` — and agrees with `μ` on `𝓕ᴮ_T`.
* `emm_unique_of_complete` — **EMM uniqueness from completeness**, on `ContinuousMarket.IsEMM`.
-/

@[expose] public section

namespace MathFin

open MeasureTheory ProbabilityTheory
open ItoIntegralCLM ItoIntegralL2 ItoIntegralProcessGeneral
open scoped NNReal ENNReal

variable {Ω : Type*} [mΩ : MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
  {B : ℝ≥0 → Ω → ℝ} (hB : IsPreBrownianReal B μ)

/-! ### Replication -/

/-- `φ` **replicates** the claim `H` from initial wealth `x`: the terminal wealth
`x + ∫₀ᵀ φ dB` of the self-financing strategy holding `φ` is `H`, almost everywhere. Reading
the Itô integral as the traded gain fixes the normalisation, and it is the only place this
file leaves `S` behind: the discounted price *is* `B` (a Bachelier-type market), so `φ` counts
units held and `∫₀ᵀ φ dB` is what holding them earns — the general `S` returns only in
`emm_unique_of_complete`, where it is *not* identified with `B`. -/
def Replicates (T : ℝ≥0) (hBmeas : ∀ t, Measurable (B t)) (x : ℝ)
    (φ : Lp ℝ 2 (trimMeasure_T (μ := μ) T hBmeas)) (H : Ω → ℝ) : Prop :=
  H =ᵐ[μ] fun ω ↦ x + itoIntegralCLM_T hB T hBmeas φ ω

/-- **The Brownian market is complete.** Every square-integrable `𝓕ᴮ_T`-claim is replicated from
initial wealth `𝔼_μ[H]`, and the hedge is unique. This is the terminal martingale representation
theorem read as a trading statement: the price is the reference expectation because the
integrand it produces has zero mean, and the integrand *is* the hedge. -/
theorem exists_replicating_strategy (hBmeas : ∀ t, Measurable (B t))
    (hBcont : ∀ ω, Continuous fun s : ℝ≥0 ↦ B s ω) (T : ℝ≥0) (H : Lp ℝ 2 μ)
    (hHmeas : AEStronglyMeasurable[ItoIntegralL2.natFiltration hBmeas T] (⇑H) μ) :
    ∃! φ : Lp ℝ 2 (trimMeasure_T (μ := μ) T hBmeas),
      Replicates hB T hBmeas (∫ ω, H ω ∂μ) φ (⇑H) :=
  exists_itoIntegral_representation hB hBmeas hBcont T H hHmeas

/-! ### Superreplication -/

/-- The **superreplication price** of `H`: the least initial wealth from which some
Itô-integrable strategy dominates `H` at the horizon. -/
noncomputable def superReplicationPrice (T : ℝ≥0) (hBmeas : ∀ t, Measurable (B t))
    (H : Ω → ℝ) : ℝ :=
  sInf {x : ℝ | ∃ φ : Lp ℝ 2 (trimMeasure_T (μ := μ) T hBmeas),
    H ≤ᵐ[μ] fun ω ↦ x + itoIntegralCLM_T hB T hBmeas φ ω}

/-- **No superreplication cost undercuts the price.** Integrating `H ≤ x + ∫₀ᵀ φ dB` kills the
Itô integral (`integral_itoIntegralCLM_T`) and leaves `𝔼_μ[H] ≤ x`. -/
private theorem integral_le_of_superReplicates (T : ℝ≥0) (hBmeas : ∀ t, Measurable (B t))
    (H : Lp ℝ 2 μ) {x : ℝ} {φ : Lp ℝ 2 (trimMeasure_T (μ := μ) T hBmeas)}
    (hφ : (⇑H) ≤ᵐ[μ] fun ω ↦ x + itoIntegralCLM_T hB T hBmeas φ ω) :
    ∫ ω, H ω ∂μ ≤ x := by
  have hgain : Integrable (itoIntegralCLM_T hB T hBmeas φ) μ :=
    (Lp.memLp (itoIntegralCLM_T hB T hBmeas φ)).integrable one_le_two
  have hdom : Integrable (fun ω ↦ x + itoIntegralCLM_T hB T hBmeas φ ω) μ :=
    (integrable_const x).add hgain
  have h := integral_mono_ae ((Lp.memLp H).integrable one_le_two) hdom hφ
  rwa [integral_add (integrable_const x) hgain, integral_itoIntegralCLM_T, integral_const,
    probReal_univ, one_smul, add_zero] at h

/-- **Superreplication duality in continuous time.** The least initial wealth from which an
Itô-integrable strategy dominates a square-integrable `𝓕ᴮ_T`-claim is exactly its price
`𝔼_μ[H]`. One inequality is that the exact replicating strategy is in particular a
superreplicating one; the other is that every superreplication cost dominates the price. -/
theorem superReplication_eq_emm_price (hBmeas : ∀ t, Measurable (B t))
    (hBcont : ∀ ω, Continuous fun s : ℝ≥0 ↦ B s ω) (T : ℝ≥0) (H : Lp ℝ 2 μ)
    (hHmeas : AEStronglyMeasurable[ItoIntegralL2.natFiltration hBmeas T] (⇑H) μ) :
    superReplicationPrice hB T hBmeas (⇑H) = ∫ ω, H ω ∂μ := by
  have hlb (x : ℝ) (hx : ∃ φ : Lp ℝ 2 (trimMeasure_T (μ := μ) T hBmeas),
      (⇑H) ≤ᵐ[μ] fun ω ↦ x + itoIntegralCLM_T hB T hBmeas φ ω) : ∫ ω, H ω ∂μ ≤ x :=
    integral_le_of_superReplicates hB T hBmeas H hx.choose_spec
  obtain ⟨φ, hφ, -⟩ := exists_replicating_strategy hB hBmeas hBcont T H hHmeas
  have hmem : ∃ ψ : Lp ℝ 2 (trimMeasure_T (μ := μ) T hBmeas),
      (⇑H) ≤ᵐ[μ] fun ω ↦ (∫ ω, H ω ∂μ) + itoIntegralCLM_T hB T hBmeas ψ ω :=
    ⟨φ, Filter.EventuallyEq.le hφ⟩
  exact le_antisymm (csInf_le ⟨_, hlb⟩ hmem) (le_csInf ⟨_, hmem⟩ hlb)

/-! ### The pricing measure -/

/-- `Q` **prices the traded gains at zero**: every terminal Itô integral against `B` on `[0,T]`
is `Q`-integrable with zero `Q`-mean. This is what it means for the strategy class to be a fair
game under `Q`, and it is what a stochastic integral against the price process would deliver
from `ContinuousMarket.IsEMM`. -/
def PricesGainsAtZero (T : ℝ≥0) (hBmeas : ∀ t, Measurable (B t)) (Q : Measure Ω) : Prop :=
  ∀ φ : Lp ℝ 2 (trimMeasure_T (μ := μ) T hBmeas),
    Integrable (itoIntegralCLM_T hB T hBmeas φ) Q ∧
      ∫ ω, itoIntegralCLM_T hB T hBmeas φ ω ∂Q = 0

/-- **The hypothesis has a witness**: the reference measure prices its own traded gains at zero,
the Itô integral being centered. -/
theorem pricesGainsAtZero_self (T : ℝ≥0) (hBmeas : ∀ t, Measurable (B t)) :
    PricesGainsAtZero hB T hBmeas μ := fun φ ↦
  ⟨(Lp.memLp (itoIntegralCLM_T hB T hBmeas φ)).integrable one_le_two,
    integral_itoIntegralCLM_T hB T hBmeas φ⟩

/-- A `Q`-martingale started at `0` has zero mean at every time: condition down to time `0`,
where `integral_condExp` preserves the mean. -/
private theorem integral_eq_zero_of_martingale_zero_start {Q : Measure Ω} [IsFiniteMeasure Q]
    {𝓖 : Filtration ℝ≥0 mΩ} {V : ℝ≥0 → Ω → ℝ} (hV : Martingale V 𝓖 Q) (hV0 : V 0 =ᵐ[Q] 0)
    (t : ℝ≥0) : ∫ ω, V t ω ∂Q = 0 := by
  rw [← integral_condExp (𝓖.le 0), integral_congr_ae ((hV.2 0 t zero_le).trans hV0)]
  simp

/-- **The centering hypothesis is the textbook one.** If every integrand's gains *process* is a
`Q`-martingale that starts at `0` and ends at `∫₀ᵀ φ dB`, then `Q` prices the traded gains at
zero. Stated over an abstract family of wealth processes so that it applies to whatever
construction supplies them — in this repo `itoProcessCLM`, in a theory with `∫ φ dS` the
self-financing wealth of the hedge. -/
theorem pricesGainsAtZero_of_gains_martingale (T : ℝ≥0) (hBmeas : ∀ t, Measurable (B t))
    {Q : Measure Ω} [IsFiniteMeasure Q]
    {V : Lp ℝ 2 (trimMeasure_T (μ := μ) T hBmeas) → ℝ≥0 → Ω → ℝ}
    (hmart : ∀ φ, Martingale (V φ) (ItoIntegralL2.natFiltration hBmeas) Q)
    (hzero : ∀ φ, V φ 0 =ᵐ[Q] 0)
    (hterm : ∀ φ, V φ T =ᵐ[Q] itoIntegralCLM_T hB T hBmeas φ) :
    PricesGainsAtZero hB T hBmeas Q := fun φ ↦
  ⟨((hmart φ).integrable T).congr (hterm φ),
    (integral_congr_ae (hterm φ)).symm.trans
      (integral_eq_zero_of_martingale_zero_start (hmart φ) (hzero φ) T)⟩

/-- **A replicated claim is worth its initial wealth** under any measure that prices the traded
gains at zero: transport the replication a.e. equality along `Q ≪ μ`, then integrate. -/
private theorem integral_eq_of_replicates (T : ℝ≥0) (hBmeas : ∀ t, Measurable (B t))
    {Q : Measure Ω} [IsProbabilityMeasure Q] (hQ : Q ≪ μ)
    (hg : PricesGainsAtZero hB T hBmeas Q) {x : ℝ}
    {φ : Lp ℝ 2 (trimMeasure_T (μ := μ) T hBmeas)} {H : Ω → ℝ}
    (hrep : Replicates hB T hBmeas x φ H) :
    ∫ ω, H ω ∂Q = x := by
  obtain ⟨hint, h0⟩ := hg φ
  rw [integral_congr_ae (Filter.Eventually.filter_mono hQ.ae_le hrep),
    integral_add (integrable_const x) hint, h0, integral_const, probReal_univ, one_smul, add_zero]

/-- **Every gains-neutral measure prices every claim at the reference expectation.** Completeness
supplies a replicating strategy; the strategy's gains are worth zero under `Q`, so only the
initial wealth `𝔼_μ[H]` survives. -/
theorem integral_eq_of_pricesGainsAtZero (hBmeas : ∀ t, Measurable (B t))
    (hBcont : ∀ ω, Continuous fun s : ℝ≥0 ↦ B s ω) (T : ℝ≥0) {Q : Measure Ω}
    [IsProbabilityMeasure Q] (hQ : Q ≪ μ) (hg : PricesGainsAtZero hB T hBmeas Q) (H : Lp ℝ 2 μ)
    (hHmeas : AEStronglyMeasurable[ItoIntegralL2.natFiltration hBmeas T] (⇑H) μ) :
    ∫ ω, H ω ∂Q = ∫ ω, H ω ∂μ := by
  obtain ⟨φ, hφ, -⟩ := exists_replicating_strategy hB hBmeas hBcont T H hHmeas
  exact integral_eq_of_replicates hB T hBmeas hQ hg hφ

/-- Anything a.e. equal to the indicator of `A` integrates to `ν A`. -/
private theorem integral_eq_measure_toReal {ν : Measure Ω} [IsFiniteMeasure ν] {A : Set Ω}
    (hA : MeasurableSet A) {f : Ω → ℝ} (hf : f =ᵐ[ν] A.indicator fun _ ↦ (1 : ℝ)) :
    ∫ ω, f ω ∂ν = (ν A).toReal := by
  rw [integral_congr_ae hf, integral_indicator hA]
  simp [Measure.real]

/-- **`μ` is the pricing measure.** A probability measure dominated by `μ` that prices the traded
gains at zero agrees with `μ` on the whole of `𝓕ᴮ_T`: apply the claim-level statement to the
indicator of the event, which is a bounded `𝓕ᴮ_T`-measurable claim. -/
theorem measure_eq_of_pricesGainsAtZero (hBmeas : ∀ t, Measurable (B t))
    (hBcont : ∀ ω, Continuous fun s : ℝ≥0 ↦ B s ω) (T : ℝ≥0) {Q : Measure Ω}
    [IsProbabilityMeasure Q] (hQ : Q ≪ μ) (hg : PricesGainsAtZero hB T hBmeas Q) {A : Set Ω}
    (hA : MeasurableSet[ItoIntegralL2.natFiltration hBmeas T] A) :
    Q A = μ A := by
  have hA' : MeasurableSet A := (ItoIntegralL2.natFiltration hBmeas).le T A hA
  have hmem : MemLp (A.indicator fun _ ↦ (1 : ℝ)) 2 μ :=
    memLp_indicator_const 2 hA' 1 (Or.inr (measure_ne_top μ A))
  have hclaim := integral_eq_of_pricesGainsAtZero hB hBmeas hBcont T hQ hg
    (hmem.toLp (A.indicator fun _ ↦ (1 : ℝ)))
    ((stronglyMeasurable_const.indicator hA).aestronglyMeasurable.congr hmem.coeFn_toLp.symm)
  have h : (Q A).toReal = (μ A).toReal :=
    ((integral_eq_measure_toReal (ν := Q) hA'
        (Filter.Eventually.filter_mono hQ.ae_le hmem.coeFn_toLp)).symm.trans hclaim).trans
      (integral_eq_measure_toReal (ν := μ) hA' hmem.coeFn_toLp)
  rw [← ENNReal.ofReal_toReal (measure_ne_top Q A),
    ← ENNReal.ofReal_toReal (measure_ne_top μ A), h]

/-- **EMM uniqueness from completeness** — the second FTAP in the direction completeness gives.
Two equivalent martingale measures for the discounted price `S` that price the traded gains at
zero agree on `𝓕ᴮ_T`, both being `μ` there. Only `isProb` and `ac` of `IsEMM` are consumed: the
`Q`-martingale property of `S` is what would *supply* `PricesGainsAtZero` in a theory with the
stochastic integral `∫ φ dS`, which is exactly the hypothesis stated here instead. See the
module docstring for why this replaces the `S`-only statement, and for the converse's scope. -/
theorem emm_unique_of_complete (hBmeas : ∀ t, Measurable (B t))
    (hBcont : ∀ ω, Continuous fun s : ℝ≥0 ↦ B s ω) (T : ℝ≥0) {S : ℝ≥0 → Ω → ℝ}
    {Q₁ Q₂ : Measure Ω}
    (h₁ : ContinuousMarket.IsEMM (P := μ) (𝓕 := ItoIntegralL2.natFiltration hBmeas) S Q₁)
    (h₂ : ContinuousMarket.IsEMM (P := μ) (𝓕 := ItoIntegralL2.natFiltration hBmeas) S Q₂)
    (hg₁ : PricesGainsAtZero hB T hBmeas Q₁) (hg₂ : PricesGainsAtZero hB T hBmeas Q₂)
    {A : Set Ω} (hA : MeasurableSet[ItoIntegralL2.natFiltration hBmeas T] A) :
    Q₁ A = Q₂ A :=
  haveI := h₁.isProb
  haveI := h₂.isProb
  (measure_eq_of_pricesGainsAtZero hB hBmeas hBcont T h₁.ac hg₁ hA).trans
    (measure_eq_of_pricesGainsAtZero hB hBmeas hBcont T h₂.ac hg₂ hA).symm

end MathFin