Numeraire of a product

theorem ProbabilityTheory.IsEVar.prod {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {S : Set (MeasureTheory.Measure 𝓧)} {T : Set (MeasureTheory.Measure 𝓨)} (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) (hT : ∀ μ ∈ T, MeasureTheory.IsFiniteMeasure μ) {X : 𝓧 → ENNReal} {Y : 𝓨 → ENNReal} (hX : IsEVar X S) (hY : IsEVar Y T) : IsEVar (fun (x : 𝓧 × 𝓨) => X x.1 * Y x.2) (Function.uncurry MeasureTheory.Measure.prod '' S ×ˢ T)

The product of the two e-variables is an e-variable for the product measure with respect to the product of the two sets.

theorem ProbabilityTheory.isNumeraire_mul {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {S : Set (MeasureTheory.Measure 𝓧)} {T : Set (MeasureTheory.Measure 𝓨)} (P : MeasureTheory.Measure 𝓧) [MeasureTheory.IsFiniteMeasure P] (Q : MeasureTheory.Measure 𝓨) [MeasureTheory.IsFiniteMeasure Q] (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) (hT : ∀ μ ∈ T, MeasureTheory.IsFiniteMeasure μ) {X : 𝓧 → ENNReal} {Y : 𝓨 → ENNReal} (hX : IsNumeraire X S P) (hY : IsNumeraire Y T Q) : IsNumeraire (fun (x : 𝓧 × 𝓨) => X x.1 * Y x.2) {ρ : MeasureTheory.Measure (𝓧 × 𝓨) | ∃ μ ∈ S, ∃ ν ∈ T, μ.prod ν = ρ} (P.prod Q)

The numeraire of a product measure with respect to a product of sets is the product of the numeraires.

theorem ProbabilityTheory.isNumeraire_mul_numeraire {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {S : Set (MeasureTheory.Measure 𝓧)} {T : Set (MeasureTheory.Measure 𝓨)} (P : MeasureTheory.Measure 𝓧) [MeasureTheory.IsFiniteMeasure P] (Q : MeasureTheory.Measure 𝓨) [MeasureTheory.IsFiniteMeasure Q] (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) (hT : ∀ μ ∈ T, MeasureTheory.IsFiniteMeasure μ) : IsNumeraire (fun (x : 𝓧 × 𝓨) => numeraire P S x.1 * numeraire Q T x.2) {ρ : MeasureTheory.Measure (𝓧 × 𝓨) | ∃ μ ∈ S, ∃ ν ∈ T, μ.prod ν = ρ} (P.prod Q)

The numeraire of a product measure with respect to a product of sets is the product of the numeraires.

theorem ProbabilityTheory.logUtility_numeraire_prod' {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {P : MeasureTheory.Measure 𝓧} {Q : MeasureTheory.Measure 𝓨} {S : Set (MeasureTheory.Measure 𝓧)} {T : Set (MeasureTheory.Measure 𝓨)} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure Q] (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) (hT : ∀ μ ∈ T, MeasureTheory.IsFiniteMeasure μ) : ∫ᵉ (x : 𝓧 × 𝓨), (numeraire (P.prod Q) (Function.uncurry MeasureTheory.Measure.prod '' S ×ˢ T) x).log ∂P.prod Q = ↑(Q Set.univ) * ∫ᵉ (x : 𝓧), (numeraire P S x).log ∂P + ↑(P Set.univ) * ∫ᵉ (x : 𝓨), (numeraire Q T x).log ∂Q

The logarithmic utility of the numeraire on a product is a weighted sum of the two logarithmic utilities.

theorem ProbabilityTheory.logUtility_numeraire_prod {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {P : MeasureTheory.Measure 𝓧} {Q : MeasureTheory.Measure 𝓨} {S : Set (MeasureTheory.Measure 𝓧)} {T : Set (MeasureTheory.Measure 𝓨)} [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) (hT : ∀ μ ∈ T, MeasureTheory.IsFiniteMeasure μ) : ∫ᵉ (x : 𝓧 × 𝓨), (numeraire (P.prod Q) (Function.uncurry MeasureTheory.Measure.prod '' S ×ˢ T) x).log ∂P.prod Q = ∫ᵉ (x : 𝓧), (numeraire P S x).log ∂P + ∫ᵉ (x : 𝓨), (numeraire Q T x).log ∂Q

The logarithmic utility of the numeraire on a product is the sum of the two logarithmic utilities.

theorem ProbabilityTheory.maxUtility_prod {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {S : Set (MeasureTheory.Measure 𝓧)} {T : Set (MeasureTheory.Measure 𝓨)} (P : MeasureTheory.Measure 𝓧) (Q : MeasureTheory.Measure 𝓨) [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) (hT : ∀ μ ∈ T, MeasureTheory.IsFiniteMeasure μ) : maxUtility (P.prod Q) (Function.uncurry MeasureTheory.Measure.prod '' S ×ˢ T) logUtility = maxUtility P S logUtility + maxUtility Q T logUtility

theorem ProbabilityTheory.iSup_prod_le_maxUtility {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {S : Set (MeasureTheory.Measure 𝓧)} (P : MeasureTheory.Measure (𝓧 × 𝓨)) {T : Set (MeasureTheory.Measure 𝓨)} (hS : ∀ μ ∈ S, MeasureTheory.IsFiniteMeasure μ) (hT : ∀ μ ∈ T, MeasureTheory.IsFiniteMeasure μ) : ⨆ (X : 𝓧 → ENNReal), ⨆ (Y : 𝓨 → ENNReal), ⨆ (_ : NeBotUtilityEVar X (MeasureTheory.Measure.map Prod.fst P) S logUtility), ⨆ (_ : NeBotUtilityEVar Y (MeasureTheory.Measure.map Prod.snd P) T logUtility), ∫ᵉ (x : 𝓧 × 𝓨), (logUtility.toFun ∘ fun (x : 𝓧 × 𝓨) => X x.1 * Y x.2) x ∂P ≤ maxUtility P (Function.uncurry MeasureTheory.Measure.prod '' S ×ˢ T) logUtility

theorem ProbabilityTheory.isNumeraire_prod_numeraire_fintype {ι : Type u_3} {𝓧 : ι → Type u_4} [hι : Fintype ι] {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {P : (i : ι) → MeasureTheory.Measure (𝓧 i)} {S : (i : ι) → Set (MeasureTheory.Measure (𝓧 i))} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (P i)] (hS : ∀ (i : ι), ∀ μ ∈ S i, MeasureTheory.IsProbabilityMeasure μ) : IsNumeraire (fun (x : (i : ι) → 𝓧 i) => ∏ i : ι, numeraire (P i) (S i) (x i)) (MeasureTheory.Measure.pi '' Set.univ.pi S) (MeasureTheory.Measure.pi P)

theorem ProbabilityTheory.isNumeraire_prod_numeraire_finset {ι : Type u_3} {𝓧 : ι → Type u_4} {s : Finset ι} {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {P : (i : ι) → MeasureTheory.Measure (𝓧 i)} {S : (i : ι) → Set (MeasureTheory.Measure (𝓧 i))} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (P i)] (hS : ∀ i ∈ s, ∀ μ ∈ S i, MeasureTheory.IsProbabilityMeasure μ) : IsNumeraire (fun (x : (i : ↥s) → 𝓧 ↑i) => ∏ i : ↥s, numeraire (P ↑i) (S ↑i) (x i)) {μ : MeasureTheory.Measure ((i : ↥s) → 𝓧 ↑i) | ∃ (ν : (i : ι) → MeasureTheory.Measure (𝓧 i)), (∀ i ∈ s, ν i ∈ S i) ∧ (MeasureTheory.Measure.pi fun (i : ↥s) => ν ↑i) = μ} (MeasureTheory.Measure.pi fun (i : ↥s) => P ↑i)