theorem MeasureTheory.Martingale.condExp_stoppedValue_stopping_time_ae_eq_restrict_le_of_countable_range {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [OrderBot ι] [SecondCountableTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} [IsFiniteMeasure μ] {X : ι → Ω → E} {τ σ : Ω → WithTop ι} (h : Martingale X 𝓕 μ) (hRC : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) {i : ι} (hτ_le : ∀ (x : Ω), τ x ≤ ↑i) (hτ : IsStoppingTime 𝓕 τ) (hσ : IsStoppingTime 𝓕 σ) (hτ_countable_range : (Set.range τ).Countable) : μ[stoppedValue X τ | hσ.measurableSpace] =ᵐ[μ.restrict {x : Ω | τ x ≤ σ x}] stoppedValue X τ

theorem MeasureTheory.Martingale.stoppedValue_min_ae_eq_condExp_of_countable_range {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [OrderBot ι] [SecondCountableTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} [IsFiniteMeasure μ] {X : ι → Ω → E} {τ σ : Ω → WithTop ι} (h : Martingale X 𝓕 μ) (hRC : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) (hτ : IsStoppingTime 𝓕 τ) (hσ : IsStoppingTime 𝓕 σ) {n : ι} (hτ_le : ∀ (x : Ω), τ x ≤ ↑n) (hτ_countable_range : (Set.range τ).Countable) (hσ_countable_range : (Set.range σ).Countable) : (stoppedValue X fun (x : Ω) => min (σ x) (τ x)) =ᵐ[μ] μ[stoppedValue X τ | hσ.measurableSpace]

theorem MeasureTheory.Martingale.stoppedValue_min_ae_eq_condExp_of_discreteApproxSequence {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [OrderBot ι] [SecondCountableTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} [IsFiniteMeasure μ] {X : ι → Ω → E} {τ σ : Ω → WithTop ι} (h : Martingale X 𝓕 μ) (hRC : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) (hτ : IsStoppingTime 𝓕 τ) (hσ : IsStoppingTime 𝓕 σ) {n : ι} (hτ_le : ∀ (x : Ω), τ x ≤ ↑n) (τn : DiscreteApproxSequence 𝓕 τ μ) (σn : DiscreteApproxSequence 𝓕 σ μ) : (stoppedValue X fun (x : Ω) => min (τ x) (σ x)) =ᵐ[μ] μ[stoppedValue X τ | hσ.measurableSpace]

Optional sampling theorem for general time indices (assuming existence of DiscreteApproxSequence).

theorem MeasureTheory.Martingale.stoppedValue_min_ae_eq_condExp' {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [OrderBot ι] [SecondCountableTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} [IsFiniteMeasure μ] {X : ι → Ω → E} {τ σ : Ω → WithTop ι} [Approximable 𝓕 μ] (h : Martingale X 𝓕 μ) (hRC : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) (hτ : IsStoppingTime 𝓕 τ) (hσ : IsStoppingTime 𝓕 σ) {n : ι} (hτ_le : ∀ (x : Ω), τ x ≤ ↑n) : (stoppedValue X fun (x : Ω) => min (τ x) (σ x)) =ᵐ[μ] μ[stoppedValue X τ | hσ.measurableSpace]

Optional sampling theorem for approximable time indices.

theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_const' {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [OrderBot ι] [SecondCountableTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} [IsFiniteMeasure μ] {X : ι → Ω → E} {τ : Ω → WithTop ι} {n : ι} [Approximable 𝓕 μ] (h : Martingale X 𝓕 μ) (hRC : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) (hτ : IsStoppingTime 𝓕 τ) (hτ_le : ∀ (x : Ω), τ x ≤ ↑n) : stoppedValue X τ =ᵐ[μ] μ[X n | hτ.measurableSpace]

theorem MeasureTheory.Martingale.condExp_stoppedValue_ae_eq_stoppedProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [OrderBot ι] [SecondCountableTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} [IsFiniteMeasure μ] {X : ι → Ω → E} {τ : Ω → WithTop ι} [Approximable 𝓕 μ] {n : ι} (h : Martingale X 𝓕 μ) (hRC : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) (hτ : IsStoppingTime 𝓕 τ) (hτ_le : ∀ (x : Ω), τ x ≤ ↑n) (i : ι) : μ[stoppedValue X τ | ↑𝓕 i] =ᵐ[μ] MeasureTheory.stoppedProcess X τ i

theorem MeasureTheory.Martingale.stoppedProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [OrderBot ι] [SecondCountableTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} [IsFiniteMeasure μ] {X : ι → Ω → E} {τ : Ω → WithTop ι} [Approximable 𝓕 μ] [TopologicalSpace.PseudoMetrizableSpace ι] (h : Martingale X 𝓕 μ) (hRC : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) (hτ : IsStoppingTime 𝓕 τ) : Martingale (MeasureTheory.stoppedProcess X τ) 𝓕 μ

theorem MeasureTheory.Submartingale.stoppedValue_min_ae_le_condExp_nat {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {σ τ : Ω → WithTop ℕ} {X : ℕ → Ω → E} (𝓕 : Filtration ℕ mΩ) [PartialOrder E] [OrderClosedTopology E] [IsOrderedModule ℝ E] [IsOrderedAddMonoid E] [SigmaFiniteFiltration P 𝓕] (hX : Submartingale X 𝓕 P) {k : ℕ} (hτk : ∀ᵐ (ω : Ω) ∂P, τ ω ≤ ↑k) (hσ : IsStoppingTime 𝓕 σ) (hτ : IsStoppingTime 𝓕 τ) : stoppedValue X (τ ⊓ σ) ≤ᵐ[P] P[stoppedValue X τ | hσ.measurableSpace]

theorem MeasureTheory.Supermartingale.condExp_ae_le_stoppedValue_min_nat {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {σ τ : Ω → WithTop ℕ} {X : ℕ → Ω → E} (𝓕 : Filtration ℕ mΩ) [PartialOrder E] [OrderClosedTopology E] [IsOrderedModule ℝ E] [IsOrderedAddMonoid E] [SigmaFiniteFiltration P 𝓕] (hX : Supermartingale X 𝓕 P) {k : ℕ} (hτk : ∀ᵐ (ω : Ω) ∂P, τ ω ≤ ↑k) (hσ : IsStoppingTime 𝓕 σ) (hτ : IsStoppingTime 𝓕 τ) : P[stoppedValue X τ | hσ.measurableSpace] ≤ᵐ[P] stoppedValue X (τ ⊓ σ)

theorem MeasureTheory.Submartingale.stoppedValue_min_ae_le_condExp {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {ι : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [OrderBot ι] [MeasurableSpace ι] [SecondCountableTopology ι] [BorelSpace ι] [TopologicalSpace.MetrizableSpace ι] {σ τ : Ω → WithTop ι} {X : ι → Ω → E} (𝓕 : Filtration ι mΩ) [PartialOrder E] [OrderClosedTopology E] [IsOrderedModule ℝ E] [IsOrderedAddMonoid E] (hX1 : Submartingale X 𝓕 P) (hX2 : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) {k : ι} (hτk : ∀ᵐ (ω : Ω) ∂P, τ ω ≤ ↑k) (hσ : IsStoppingTime 𝓕 σ) (hτ : IsStoppingTime 𝓕 τ) : stoppedValue X (τ ⊓ σ) ≤ᵐ[P] P[stoppedValue X τ | hσ.measurableSpace]