StationaryMoment.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.StationaryMoment.integral_partition_pushforwards line 23

Source documentation

A partition expressed by scaled pushforward laws gives its weighted quadratic-potential integral identity.

theorem integral_partition_pushforwards
    (μ : ι → Measure A) [∀ i, IsFiniteMeasure (μ i)]
    (X : ι → A → F) (w : ι → ℝ) (ρ : Measure F) (R : ℝ)
    (hX : ∀ i, MemLp (X i) 2 (μ i)) (hw : ∀ i, 0 ≤ w i)
    (hpartition : (∑ i, ENNReal.ofReal (w i) • Measure.map (X i) (μ i)) = ρ) :
    (∫ x, quadraticPotential R x ∂ρ) =
      ∑ i, w i * ∫ a, quadraticPotential R (X i a) ∂μ i := by
…

theorem OAI.Problem358.StationaryMoment.conditional_stationary_moment_finite_difference line 48

Source documentation

The full finite-difference moment estimate assembled from actual midpoint measure domination and endpoint partition laws. The existence of those dominated couplings is an explicit input, not a conclusion of this theorem.

theorem conditional_stationary_moment_finite_difference
    (μ : ι → Measure A) [∀ i, IsProbabilityMeasure (μ i)]
    (X Z : ι → A → F) (η : ι → Measure F) (ρ : Measure F)
    [∀ i, IsFiniteMeasure (η i)]
    (M α β γ : ι → ℝ) {R : ℝ}
    (hX : ∀ i, MemLp (X i) 2 (μ i)) (hZ : ∀ i, MemLp (Z i) 2 (μ i))
    (hR : 0 ≤ R) (hM : ∀ i, 0 < M i)
    (hα : ∀ i, 0 ≤ α i) (hβ : ∀ i, 0 ≤ β i)
    (hαM : ∀ i, α i ≤ 2 * M i) (hγM : ∀ i, M i / 2 ≤ γ i)
    (hγsq : ∀ i, γ i ^ 2 = α i * β i)
    (hXR : ∀ i, ∀ᵐ a ∂μ i, ‖X i a‖ ≤ R)
    (hZR : ∀ i, ∀ᵐ a ∂μ i, ‖Z i a‖ ≤ R)
…

structure OAI.Problem358.StationaryMoment.MidpointComparisonData line 124
Source documentation
Geometric data sufficient for one symmetric cell-moment comparison. In particular, midpoint_dominated records the difficult geometric input.
```
structure MidpointComparisonData (Ω : Type*) [MeasurableSpace Ω]
    (M α β : ι → ℝ) (Δ : ι → F) (ρ : Measure F) (R : ℝ) where
…
```

theorem OAI.Problem358.StationaryMoment.MidpointComparisonData.finite_difference line 153

Source documentation

A packaged midpoint comparison proves the uniform finite-difference bound.

theorem MidpointComparisonData.finite_difference
    {M α β : ι → ℝ} {Δ : ι → F} {ρ : Measure F} {R : ℝ}
    (data : MidpointComparisonData A M α β Δ ρ R)
    (hR : 0 ≤ R) (hM : ∀ i, 0 < M i) :
    (∑ i, ‖Δ i‖ ^ 2 / M i) ≤ 162 * R ^ 2 * ∑ i, (α i - β i) ^ 2 / M i := by
…

Mentions: OAI.Problem358.StationaryMoment.MidpointComparisonData

theorem OAI.Problem358.StationaryMoment.stationary_moment_derivative_of_midpoint_data line 171

Source documentation

Conditional stationary-site derivative estimate. Its inputs are ordinary derivatives and actual midpoint comparison data for sufficiently small positive perturbations; no quantitative limiting inequality is assumed.

theorem stationary_moment_derivative_of_midpoint_data
    {B : ι → ℝ → F} {m : ι → ℝ → ℝ} {dB : ι → F} {dm M : ι → ℝ}
    {ρ : Measure F} {R : ℝ}
    (hR : 0 ≤ R) (hM : ∀ i, 0 < M i)
    (hB : ∀ i, HasDerivAt (B i) (dB i) 0)
    (hm : ∀ i, HasDerivAt (m i) (dm i) 0)
    (hdata : ∀ᶠ s : ℝ in 𝓝[>] 0, Nonempty
      (MidpointComparisonData A M (fun i => m i (-s)) (fun i => m i s)
        (fun i => B i (-s) - B i s) ρ R)) :
    (∑ i, ‖dB i‖ ^ 2 / M i) ≤ 162 * R ^ 2 * ∑ i, dm i ^ 2 / M i := by
…

Mentions: OAI.Problem358.StationaryMoment.MidpointComparisonData

theorem OAI.Problem358.StationaryMoment.pair_moment_difference line 202

Source documentation

Weighted pair marginals recover the raw unnormalized vector moments.

theorem pair_moment_difference
    (π : Measure (F × F)) (ρminus ρplus : Measure F) {α β : ℝ}
    (hα : 0 ≤ α) (hβ : 0 ≤ β)
    (hleft : ENNReal.ofReal α • Measure.map Prod.fst π = ρminus)
    (hright : ENNReal.ofReal β • Measure.map Prod.snd π = ρplus) :
    α • (∫ p : F × F, p.1 ∂π) - β • (∫ p : F × F, p.2 ∂π) =
      (∫ x : F, x ∂ρminus) - ∫ x : F, x ∂ρplus := by
…

def OAI.Problem358.StationaryMoment.midpointComparisonData_of_pair_couplings line 219

Source documentation

Construct the abstract moment witness directly from genuine pair couplings of the three finite cell partitions. Squared-integrability and the moment identity are consequences, rather than extra assumptions.

def midpointComparisonData_of_pair_couplings
    (π : ι → Measure (F × F)) [∀ i, IsProbabilityMeasure (π i)]
    (ρminus ρplus ρmiddle : ι → Measure F) [∀ i, IsFiniteMeasure (ρmiddle i)]
    (ρ : Measure F) (M α β γ : ι → ℝ) (R : ℝ)
    (hα : ∀ i, 0 ≤ α i) (hβ : ∀ i, 0 ≤ β i)
    (hαM : ∀ i, α i ≤ 2 * M i) (hγM : ∀ i, M i / 2 ≤ γ i)
    (hγsq : ∀ i, γ i ^ 2 = α i * β i)
    (hπ : ∀ i, ∀ᵐ p : F × F ∂π i, ‖p.1‖ ≤ R ∧ ‖p.2‖ ≤ R)
    (hmiddle : ∀ i, ∀ᵐ x : F ∂ρmiddle i, ‖x‖ ≤ R)
    (hleftLaw : ∀ i, ENNReal.ofReal (α i) • Measure.map Prod.fst (π i) = ρminus i)
    (hrightLaw : ∀ i, ENNReal.ofReal (β i) • Measure.map Prod.snd (π i) = ρplus i)
    (hleftPartition : (∑ i, ρminus i) = ρ)
…

structure OAI.Problem358.StationaryMoment.AECellPartition line 279
Source documentation
The ordinary measurable, almost-everywhere partition properties of cells.
```
structure AECellPartition (ρ : Measure F) (P : ι → Set F) : Prop where
…
```
theorem OAI.Problem358.StationaryMoment.AECellPartition.sum_restrict line 286
theorem OAI.Problem358.StationaryMoment.normalizedCellLaw_ae_norm_le line 294
Source documentation
Conditioning preserves an almost-everywhere source ball bound.
```
theorem normalizedCellLaw_ae_norm_le {ρ : Measure F} {R : ℝ}
    (hR : ∀ᵐ x ∂ρ, ‖x‖ ≤ R) (P : Set F) :
    ∀ᵐ x ∂normalizedCellLaw ρ P, ‖x‖ ≤ R :=
…
```
Mentions: OAI.Problem358.normalizedCellLaw

theorem OAI.Problem358.StationaryMoment.normalized_pair_ae_norm_le line 301

Source documentation

A normalized-cell coupling inherits both source ball bounds.

theorem normalized_pair_ae_norm_le {ρ : Measure F} {R : ℝ}
    (hR : ∀ᵐ x ∂ρ, ‖x‖ ≤ R) (P Q : Set F) (π : Measure (F × F))
    (hleft : Measure.map Prod.fst π = normalizedCellLaw ρ P)
    (hright : Measure.map Prod.snd π = normalizedCellLaw ρ Q) :
    ∀ᵐ p : F × F ∂π, ‖p.1‖ ≤ R ∧ ‖p.2‖ ≤ R := by
…

Mentions: OAI.Problem358.normalizedCellLaw

def OAI.Problem358.StationaryMoment.midpointComparisonData_of_normalized_cells line 319

Source documentation

Actual normalized couplings of three cell partitions supply the moment comparison data. All measure-scaling, partition, boundedness and raw-moment identities follow from their definitions; midpoint domination remains the explicit geometric input.

def midpointComparisonData_of_normalized_cells
    (ρ : Measure F) [IsFiniteMeasure ρ]
    (Pminus Pplus Pmiddle : ι → Set F)
    (hminus : AECellPartition ρ Pminus) (hplus : AECellPartition ρ Pplus)
    (hmiddle : AECellPartition ρ Pmiddle)
    (hminus_pos : ∀ i, ρ (Pminus i) ≠ 0) (hplus_pos : ∀ i, ρ (Pplus i) ≠ 0)
    (π : ι → Measure (F × F)) [∀ i, IsProbabilityMeasure (π i)]
    (hleft : ∀ i, Measure.map Prod.fst (π i) = normalizedCellLaw ρ (Pminus i))
    (hright : ∀ i, Measure.map Prod.snd (π i) = normalizedCellLaw ρ (Pplus i))
    (M γ : ι → ℝ) (R : ℝ) (hR : ∀ᵐ x ∂ρ, ‖x‖ ≤ R)
    (hαM : ∀ i, ρ.real (Pminus i) ≤ 2 * M i)
    (hγM : ∀ i, M i / 2 ≤ γ i)
…

Mentions: OAI.Problem358.StationaryMoment.AECellPartition, OAI.Problem358.normalizedCellLaw

structure OAI.Problem358.StationaryMoment.NormalizedMidpointWitness line 362
Source documentation
A genuine pair law with normalized cell marginals and the geometric midpoint domination. No moment inequality is a field of this witness.
```
structure NormalizedMidpointWitness (ρ : Measure F) (P Q H : ι → Set F) where
…
```

theorem OAI.Problem358.StationaryMoment.stationary_moment_derivative_of_normalized_cells line 374

Source documentation

The stationary-site moment derivative bound for actual moving cells. Only ordinary derivatives and genuine normalized midpoint couplings are assumed. All nearby mass comparisons follow from continuity.

theorem stationary_moment_derivative_of_normalized_cells
    (ρ : Measure F) [IsFiniteMeasure ρ] (P : ℝ → ι → Set F)
    (hP : ∀ s, AECellPartition ρ (P s))
    (R : ℝ) (hR : 0 ≤ R) (hbounded : ∀ᵐ x ∂ρ, ‖x‖ ≤ R)
    (dB : ι → F) (dm : ι → ℝ)
    (hM : ∀ i, 0 < ρ.real (P 0 i))
    (hB : ∀ i, HasDerivAt (fun s => ∫ x in P s i, x ∂ρ) (dB i) 0)
    (hm : ∀ i, HasDerivAt (fun s => ρ.real (P s i)) (dm i) 0)
    (hw : ∀ᶠ s : ℝ in 𝓝[>] 0,
      Nonempty (NormalizedMidpointWitness ρ (P (-s)) (P s) (P 0))) :
    (∑ i, ‖dB i‖ ^ 2 / ρ.real (P 0 i)) ≤
      162 * R ^ 2 * ∑ i, dm i ^ 2 / ρ.real (P 0 i) := by
…

Mentions: OAI.Problem358.StationaryMoment.AECellPartition, OAI.Problem358.StationaryMoment.NormalizedMidpointWitness

theorem OAI.Problem358.CellGeometry.aePartition_uniform_closedCell line 425

Source documentation

The actual distinct-site closed cells form the normalized source partition.

theorem aePartition_uniform_closedCell {d : ℕ} {ι : Type*}
    [Fintype ι] [Nonempty ι] {K : Set (E d)} (hK : IsClosed K)
    (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y) :
    StationaryMoment.AECellPartition (uniformMeasure K) (closedCell K y c) where
…

Mentions: OAI.Problem358.StationaryMoment.AECellPartition, OAI.Problem358.CellGeometry.closedCell

theorem OAI.Problem358.CellGeometry.ofReal_sqrt_uniform_cell_masses line 437

Source documentation

The raw-volume geometric mean converts to the geometric mean of normalized cell masses with exactly one source-volume factor.

theorem ofReal_sqrt_uniform_cell_masses {d : ℕ} {K U V : Set (E d)}
    (hKpos : 0 < volume K) (hKfinite : volume K ≠ ∞)
    (hU : MeasurableSet U) (hV : MeasurableSet V) (hUK : U ⊆ K) (hVK : V ⊆ K) :
    ENNReal.ofReal (Real.sqrt ((uniformMeasure K).real U * (uniformMeasure K).real V)) =
      (volume K)⁻¹ * ENNReal.ofReal (Real.sqrt ((volume U).toReal * (volume V).toReal)) := by
…

theorem OAI.Problem358.CellGeometry.normalized_midpoint_domination line 453

Source documentation

A raw midpoint coupling supported by a middle cell yields the exact normalized restricted domination used in the stationary moment estimate.

theorem normalized_midpoint_domination {d : ℕ} {K U V H : Set (E d)}
    (hKpos : 0 < volume K) (hKfinite : volume K ≠ ∞)
    (hU : MeasurableSet U) (hV : MeasurableSet V) (hH : MeasurableSet H)
    (hUK : U ⊆ K) (hVK : V ⊆ K) (hHK : H ⊆ K)
    {π : Measure (E d × E d)}
    (hπ : IsCoupling (uniformMeasure U) (uniformMeasure V) π)
    (hsupport : ∀ x ∈ U, ∀ z ∈ V, (1 / 2 : ℝ) • (x + z) ∈ H)
    (hdom : ENNReal.ofReal (Real.sqrt ((volume U).toReal * (volume V).toReal)) •
      Measure.map (fun p : E d × E d => (1 / 2 : ℝ) • (p.1 + p.2)) π ≤ volume) :
    ENNReal.ofReal (Real.sqrt ((uniformMeasure K).real U * (uniformMeasure K).real V)) •
      Measure.map (fun p : E d × E d => (1 / 2 : ℝ) • (p.1 + p.2)) π ≤
        (uniformMeasure K).restrict H := by
…

theorem OAI.Problem358.CellGeometry.normalized_witness_closedCells line 488

Source documentation

A raw dominated coupling of the two opposite intercept cells supplies the exact normalized cell witness, with all support and normalization requirements derived from the actual affine cell geometry.

theorem normalized_witness_closedCells {d : ℕ} {ι : Type*} [Fintype ι]
    {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
    (hKi : (interior K).Nonempty) (y : ι → E d) (c q : ι → ℝ) (s : ℝ)
    (hraw : ∀ i, ∃ π : Measure (E d × E d),
      IsCoupling (uniformMeasure (closedCell K y (fun j => c j - s * q j) i))
        (uniformMeasure (closedCell K y (fun j => c j + s * q j) i)) π ∧
      ENNReal.ofReal (Real.sqrt
        ((volume (closedCell K y (fun j => c j - s * q j) i)).toReal *
          (volume (closedCell K y (fun j => c j + s * q j) i)).toReal)) •
        Measure.map (fun p : E d × E d => (1 / 2 : ℝ) • (p.1 + p.2)) π ≤ volume) :
    Nonempty (StationaryMoment.NormalizedMidpointWitness (uniformMeasure K)
      (closedCell K y (fun j => c j - s * q j))
…

Mentions: OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.StationaryMoment.NormalizedMidpointWitness

theorem OAI.Problem358.CellGeometry.stationary_moment_derivative_of_convex_midpoint line 541

Source documentation

Stationary-site moment coercivity for the actual affine cells. The only geometric input not supplied internally is the convex-body midpoint coupling; ordinary mass and moment derivatives are left in the form delivered by cell calculus. In particular no cell partition, scaled-law, nearby-mass, or energy hypothesis remains.

theorem stationary_moment_derivative_of_convex_midpoint
    {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
    {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
    (hKi : (interior K).Nonempty) (y : ι → E d) (c q : ι → ℝ)
    (hy : Function.Injective y) (R : ℝ) (hR : 0 ≤ R)
    (hbounded : ∀ᵐ x ∂uniformMeasure K, ‖x‖ ≤ R)
    (dB : ι → E d) (dm : ι → ℝ)
    (hM : ∀ i, 0 < (uniformMeasure K).real (closedCell K y c i))
    (hB : ∀ i, HasDerivAt
      (fun s : ℝ => ∫ x in closedCell K y (fun j => c j + s * q j) i, x ∂uniformMeasure K)
      (dB i) 0)
    (hm : ∀ i, HasDerivAt
…

Mentions: OAI.Problem358.CellGeometry.closedCell