OAI/Analysis/Brenier/Midpoint.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

One-dimensional substitution estimates for midpoint-coupling constructions. These lemmas do not assume or assert existence of a triangular quantile map.

  1. def OAI.Problem358.IntervalMidpoint.unitLaw line 12

    Source documentation

    Lebesgue probability on the unit interval.

    def unitLaw : Measure ℝ := volume.restrict (Icc (0 : ℝ) 1)
  2. instance OAI.Problem358.IntervalMidpoint.unitLaw_probability line 14
  3. def OAI.Problem358.IntervalMidpoint.intervalLaw line 19

    Source documentation

    Lebesgue probability on a nondegenerate interval.

    def intervalLaw (a b : ℝ) : Measure ℝ :=
…
  4. lemma OAI.Problem358.IntervalMidpoint.map_volume_affine line 22
  5. lemma OAI.Problem358.IntervalMidpoint.affine_preimage_interval line 31
  6. lemma OAI.Problem358.IntervalMidpoint.map_unitLaw_affine line 41
  7. def OAI.Problem358.IntervalMidpoint.coupling line 49

    Source documentation

    The monotone coupling parametrized by the common unit-interval coordinate.

    def coupling (a b c d : ℝ) : Measure (ℝ × ℝ) :=
…
  8. lemma OAI.Problem358.IntervalMidpoint.coupling_fst line 52
  9. lemma OAI.Problem358.IntervalMidpoint.coupling_snd line 58
  10. lemma OAI.Problem358.IntervalMidpoint.coupling_probability line 64
  11. lemma OAI.Problem358.IntervalMidpoint.midpoint_law line 69
  12. lemma OAI.Problem358.IntervalMidpoint.sqrt_lengthProduct_le_midpoint_length line 83
  13. lemma OAI.Problem358.IntervalMidpoint.midpoint_domination line 93

    Source documentation

    The geometric-mean weighted midpoint law is dominated by Lebesgue measure on the midpoint interval. This is the genuine one-dimensional midpoint coupling.

    lemma midpoint_domination {a b c d : ℝ} (hab : a < b) (hcd : c < d) :
    ENNReal.ofReal (Real.sqrt ((b - a) * (d - c))) •
      Measure.map (fun p : ℝ × ℝ => (p.1 + p.2) / 2) (coupling a b c d) ≤
        volume.restrict (Icc ((a + c) / 2) ((b + d) / 2)) := by
…

    Mentions: OAI.Problem358.IntervalMidpoint.coupling

  14. lemma OAI.Problem358.IntervalMidpoint.intervalLaw_probability line 109
  15. theorem OAI.Problem358.IntervalMidpoint.exists_midpoint_coupling line 115

    Source documentation

    Existence formulation, including both exact marginals and probability.

    theorem exists_midpoint_coupling {a b c d : ℝ} (hab : a < b) (hcd : c < d) :
    ∃ π : Measure (ℝ × ℝ), IsProbabilityMeasure π ∧
      Measure.map Prod.fst π = intervalLaw a b ∧
      Measure.map Prod.snd π = intervalLaw c d ∧
      ENNReal.ofReal (Real.sqrt ((b - a) * (d - c))) •
        Measure.map (fun p : ℝ × ℝ => (p.1 + p.2) / 2) π ≤ volume := by
…

    Mentions: OAI.Problem358.IntervalMidpoint.intervalLaw

  16. theorem OAI.Problem358.lintegral_jacobian_comp_le line 134

    Source documentation

    Injective one-dimensional substitution followed by enlargement of the image. No measurability assumption on the nonnegative integrand is needed.

    theorem lintegral_jacobian_comp_le {s : Set ℝ} {f f' : ℝ → ℝ}
    (hs : MeasurableSet s)
    (hderiv : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x)
    (hinj : InjOn f s) (g : ℝ → ℝ≥0∞) :
    (∫⁻ x in s, ENNReal.ofReal (|f' x|) * g (f x)) ≤ ∫⁻ y, g y := by
…
  17. theorem OAI.Problem358.lintegral_comp_le_of_deriv_lower line 143

    Source documentation

    A lower Jacobian bound controls pushforward integrals.

    theorem lintegral_comp_le_of_deriv_lower {s : Set ℝ} {f f' : ℝ → ℝ} {c : ℝ}
    (hs : MeasurableSet s)
    (hderiv : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x)
    (hinj : InjOn f s) (hbound : ∀ x ∈ s, c ≤ |f' x|)
    (g : ℝ → ℝ≥0∞) :
    ENNReal.ofReal c * (∫⁻ x in s, g (f x)) ≤ ∫⁻ y, g y := by
…
  18. theorem OAI.Problem358.map_restrict_volume_smul_le_of_deriv_lower line 160

    Source documentation

    Measure-valued form of the lower-Jacobian substitution bound.

    theorem map_restrict_volume_smul_le_of_deriv_lower
    {s : Set ℝ} {f f' : ℝ → ℝ} {c : ℝ}
    (hs : MeasurableSet s)
    (hderiv : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x)
    (hinj : InjOn f s) (hbound : ∀ x ∈ s, c ≤ |f' x|) :
    ENNReal.ofReal c • Measure.map f (volume.restrict s) ≤ volume := by
…
  19. theorem OAI.Problem358.midpoint_derivative_ge_geometric_mean line 185

    Source documentation

    The derivative of the midpoint exceeds the geometric mean of the two nonnegative derivatives.

    theorem midpoint_derivative_ge_geometric_mean {u v : ℝ} (hu : 0 ≤ u) (hv : 0 ≤ v) :
    Real.sqrt (u * v) ≤ (u + v) / 2 := by
…
  20. theorem OAI.Problem358.lintegral_midpoint_geometric_jacobian_le line 194

    Source documentation

    Midpoint substitution with geometric-mean Jacobian weight. This is the one-dimensional step in the triangular domination argument.

    theorem lintegral_midpoint_geometric_jacobian_le
    {s : Set ℝ} {f f' g g' : ℝ → ℝ}
    (hs : MeasurableSet s) (hconv : Convex ℝ s)
    (hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x)
    (hg : ∀ x ∈ s, HasDerivWithinAt g (g' x) s x)
    (hfpos : ∀ x ∈ s, 0 < f' x) (hgpos : ∀ x ∈ s, 0 < g' x)
    (w : ℝ → ℝ≥0∞) :
    (∫⁻ x in s, ENNReal.ofReal (Real.sqrt (f' x * g' x)) *
      w ((f x + g x) / 2)) ≤ ∫⁻ y, w y := by
…
  21. theorem OAI.Problem358.integral_eq_weighted_sum_of_measure_partition line 245

    Source documentation

    Integration commutes with a finite weighted partition of a measure.

    theorem integral_eq_weighted_sum_of_measure_partition
    {ι X : Type*} [Fintype ι] [MeasurableSpace X]
    (ρ : Measure X) (ν : ι → Measure X) (c : ι → ℝ)
    (hc : ∀ i, 0 ≤ c i)
    (hpart : (∑ i, ENNReal.ofReal (c i) • ν i) = ρ)
    (f : X → ℝ) (hf : Integrable f ρ) :
    (∫ x, f x ∂ρ) = ∑ i, c i * ∫ x, f x ∂ν i := by
…
  22. theorem OAI.Problem358.weighted_integral_sum_le_of_measure_domination line 264

    Source documentation

    A finite family of dominated measures can be tested against any integrable function which is nonnegative almost everywhere for the dominating total.

    theorem weighted_integral_sum_le_of_measure_domination
    {ι X : Type*} [Fintype ι] [MeasurableSpace X]
    (ρ : Measure X) (μ ν : ι → Measure X) (c : ι → ℝ)
    (hc : ∀ i, 0 ≤ c i) (hpart : (∑ i, μ i) = ρ)
    (hdom : ∀ i, ENNReal.ofReal (c i) • ν i ≤ μ i)
    (f : X → ℝ) (hf : Integrable f ρ) (hfn : 0 ≤ᵐ[ρ] f) :
    (∑ i, c i * ∫ x, f x ∂ν i) ≤ ∫ x, f x ∂ρ := by
…
  23. theorem OAI.Problem358.quadratic_midpoint_identity line 287

    Source documentation

    The parallelogram identity, written for the concave quadratic test function.

    theorem quadratic_midpoint_identity {V : Type*} [NormedAddCommGroup V]
    [InnerProductSpace ℝ V] (R : ℝ) (x z : V) :
    R ^ 2 - ‖(1 / 2 : ℝ) • (x + z)‖ ^ 2 =
      ((R ^ 2 - ‖x‖ ^ 2) + (R ^ 2 - ‖z‖ ^ 2)) / 2 + ‖x - z‖ ^ 2 / 4 := by
…
  24. theorem OAI.Problem358.integral_quadratic_midpoint_identity line 297

    Source documentation

    Integrating the midpoint identity requires only the explicit integrability of its endpoint and displacement terms.

    theorem integral_quadratic_midpoint_identity
    {Ω V : Type*} [MeasurableSpace Ω] [NormedAddCommGroup V]
    [InnerProductSpace ℝ V] (μ : Measure Ω) (X Z : Ω → V) (R : ℝ)
    (hX : Integrable (fun ω => R ^ 2 - ‖X ω‖ ^ 2) μ)
    (hZ : Integrable (fun ω => R ^ 2 - ‖Z ω‖ ^ 2) μ)
    (hD : Integrable (fun ω => ‖X ω - Z ω‖ ^ 2) μ) :
    (∫ ω, R ^ 2 - ‖(1 / 2 : ℝ) • (X ω + Z ω)‖ ^ 2 ∂μ) =
      ((∫ ω, R ^ 2 - ‖X ω‖ ^ 2 ∂μ) +
        (∫ ω, R ^ 2 - ‖Z ω‖ ^ 2 ∂μ)) / 2 +
      (∫ ω, ‖X ω - Z ω‖ ^ 2 ∂μ) / 4 := by
…
  25. theorem OAI.Problem358.midpoint_partition_balance line 315

    Source documentation

    Actual dominated midpoint laws and endpoint measure partitions supply the aggregate scalar balance used by midpoint_aggregate_transport.

    theorem midpoint_partition_balance
    {ι X : Type*} [Fintype ι] [MeasurableSpace X]
    (ρ : Measure X) (cell minus plus mid : ι → Measure X)
    (α β γ D : ι → ℝ)
    (hα : ∀ i, 0 ≤ α i) (hβ : ∀ i, 0 ≤ β i) (hγ : ∀ i, 0 ≤ γ i)
    (hcells : (∑ i, cell i) = ρ)
    (hminus : (∑ i, ENNReal.ofReal (α i) • minus i) = ρ)
    (hplus : (∑ i, ENNReal.ofReal (β i) • plus i) = ρ)
    (hdom : ∀ i, ENNReal.ofReal (γ i) • mid i ≤ cell i)
    (f : X → ℝ) (hf : Integrable f ρ) (hfn : 0 ≤ᵐ[ρ] f)
    (hmid : ∀ i, (∫ x, f x ∂mid i) =
      ((∫ x, f x ∂minus i) + (∫ x, f x ∂plus i)) / 2 + D i / 4) :
…
  26. abbrev OAI.Problem358.MidpointCoordinates.Coordinates line 356
  27. def OAI.Problem358.MidpointCoordinates.coordinateUniform line 358
  28. lemma OAI.Problem358.MidpointCoordinates.volume_preimage_toLp line 362
  29. lemma OAI.Problem358.MidpointCoordinates.map_coordinateUniform line 368

    Source documentation

    The ordinary coordinate-space normalization maps to the exact source used in the challenge, with no additional volume constants.

    lemma map_coordinateUniform {d : ℕ} {K : Set (E d)} (hK : MeasurableSet K) :
    Measure.map (WithLp.toLp 2) (coordinateUniform K) = uniformMeasure K := by
…

    Mentions: OAI.Problem358.MidpointCoordinates.coordinateUniform

  30. def OAI.Problem358.MidpointCoordinates.liftPair line 376
  31. lemma OAI.Problem358.MidpointCoordinates.measurable_liftPair line 379
  32. lemma OAI.Problem358.MidpointCoordinates.liftPair_midpoint line 383
  33. lemma OAI.Problem358.MidpointCoordinates.lift_coupling line 389

    Source documentation

    Pushing both coordinates through toLp preserves both exact marginals.

    lemma lift_coupling {d : ℕ} {K L : Set (E d)}
    (hK : MeasurableSet K) (hL : MeasurableSet L)
    {π : Measure (Coordinates d × Coordinates d)}
    (hπ : IsProbabilityMeasure π)
    (hfst : Measure.map Prod.fst π = coordinateUniform K)
    (hsnd : Measure.map Prod.snd π = coordinateUniform L) :
    IsCoupling (uniformMeasure K) (uniformMeasure L) (Measure.map liftPair π) := by
…

    Mentions: OAI.Problem358.MidpointCoordinates.Coordinates, OAI.Problem358.MidpointCoordinates.coordinateUniform, OAI.Problem358.MidpointCoordinates.liftPair

  34. lemma OAI.Problem358.MidpointCoordinates.lift_midpoint_domination line 408

    Source documentation

    A weighted midpoint domination inequality survives the coordinate change.

    lemma lift_midpoint_domination {d : ℕ}
    {π : Measure (Coordinates d × Coordinates d)} {c : ℝ≥0∞}
    (hdom : c • Measure.map
      (fun p : Coordinates d × Coordinates d => (1 / 2 : ℝ) • (p.1 + p.2)) π ≤
        volume) :
    c • Measure.map (fun p : E d × E d => (1 / 2 : ℝ) • (p.1 + p.2))
      (Measure.map liftPair π) ≤ volume := by
…

    Mentions: OAI.Problem358.MidpointCoordinates.Coordinates, OAI.Problem358.MidpointCoordinates.liftPair

  35. theorem OAI.Problem358.MidpointCoordinates.exists_lifted_midpoint_coupling line 432

    Source documentation

    Coordinate-space dominated midpoint witnesses give the corresponding Euclidean-space witnesses. No existence assumption is hidden in the change of representation.

    theorem exists_lifted_midpoint_coupling {d : ℕ} {K L : Set (E d)}
    (hK : MeasurableSet K) (hL : MeasurableSet L) (c : ℝ≥0∞)
    (h : ∃ π : Measure (Coordinates d × Coordinates d), IsProbabilityMeasure π ∧
      Measure.map Prod.fst π = coordinateUniform K ∧
      Measure.map Prod.snd π = coordinateUniform L ∧
      c • Measure.map
        (fun p : Coordinates d × Coordinates d => (1 / 2 : ℝ) • (p.1 + p.2)) π ≤
        volume) :
    ∃ π : Measure (E d × E d), IsCoupling (uniformMeasure K) (uniformMeasure L) π ∧
      c • Measure.map (fun p : E d × E d => (1 / 2 : ℝ) • (p.1 + p.2)) π ≤ volume := by
…

    Mentions: OAI.Problem358.MidpointCoordinates.Coordinates, OAI.Problem358.MidpointCoordinates.coordinateUniform

  36. lemma OAI.Problem358.MidpointCoordinates.volume_interior line 447

    Source documentation

    Passing to the interior of a convex body does not change its volume.

    lemma volume_interior {d : ℕ} {K : Set (E d)} (hK : Convex ℝ K) :
    volume (interior K) = volume K :=
…
  37. lemma OAI.Problem358.MidpointCoordinates.uniformMeasure_interior line 452

    Source documentation

    The normalized law is also unchanged, including degenerate convex sets.

    lemma uniformMeasure_interior {d : ℕ} {K : Set (E d)} (hK : Convex ℝ K) :
    uniformMeasure (interior K) = uniformMeasure K := by
…
  38. theorem OAI.Problem358.MidpointCoordinates.exists_lifted_midpoint_coupling_of_interiors line 460

    Source documentation

    A construction using open convex interiors in ordinary coordinates supplies the exact closed-body laws required by the Euclidean midpoint argument.

    theorem exists_lifted_midpoint_coupling_of_interiors {d : ℕ} {K L : Set (E d)}
    (hK : Convex ℝ K) (hL : Convex ℝ L) (c : ℝ≥0∞)
    (h : ∃ π : Measure (Coordinates d × Coordinates d), IsProbabilityMeasure π ∧
      Measure.map Prod.fst π = coordinateUniform (interior K) ∧
      Measure.map Prod.snd π = coordinateUniform (interior L) ∧
      c • Measure.map
        (fun p : Coordinates d × Coordinates d => (1 / 2 : ℝ) • (p.1 + p.2)) π ≤
        volume) :
    ∃ π : Measure (E d × E d), IsCoupling (uniformMeasure K) (uniformMeasure L) π ∧
      c • Measure.map (fun p : E d × E d => (1 / 2 : ℝ) • (p.1 + p.2)) π ≤ volume := by
…

    Mentions: OAI.Problem358.MidpointCoordinates.Coordinates, OAI.Problem358.MidpointCoordinates.coordinateUniform

  39. theorem OAI.Problem358.MidpointCoordinates.exists_midpoint_coupling_of_coordinate_samplers line 475

    Source documentation

    The common-source sampler formulation constructs the joint coupling rather than requiring it as a separate input.

    theorem exists_midpoint_coupling_of_coordinate_samplers
    {Ω : Type*} [MeasurableSpace Ω] {ρ : Measure Ω} [IsProbabilityMeasure ρ]
    {d : ℕ} {K L : Set (E d)} (hK : MeasurableSet K) (hL : MeasurableSet L)
    (X Y : Ω → Coordinates d) (hX : Measurable X) (hY : Measurable Y)
    (hXlaw : Measure.map X ρ = coordinateUniform K)
    (hYlaw : Measure.map Y ρ = coordinateUniform L) (c : ℝ≥0∞)
    (hdom : c • Measure.map (fun ω => (1 / 2 : ℝ) • (X ω + Y ω)) ρ ≤ volume) :
    ∃ π : Measure (E d × E d), IsCoupling (uniformMeasure K) (uniformMeasure L) π ∧
      c • Measure.map (fun p : E d × E d => (1 / 2 : ℝ) • (p.1 + p.2)) π ≤ volume := by
…

    Mentions: OAI.Problem358.MidpointCoordinates.Coordinates, OAI.Problem358.MidpointCoordinates.coordinateUniform

  40. theorem OAI.Problem358.MidpointCoordinates.exists_midpoint_coupling_of_interior_coordinate_samplers line 495

    Source documentation

    Open-interior coordinate samplers suffice for the exact original body laws.

    theorem exists_midpoint_coupling_of_interior_coordinate_samplers
    {Ω : Type*} [MeasurableSpace Ω] {ρ : Measure Ω} [IsProbabilityMeasure ρ]
    {d : ℕ} {K L : Set (E d)} (hK : Convex ℝ K) (hL : Convex ℝ L)
    (X Y : Ω → Coordinates d) (hX : Measurable X) (hY : Measurable Y)
    (hXlaw : Measure.map X ρ = coordinateUniform (interior K))
    (hYlaw : Measure.map Y ρ = coordinateUniform (interior L)) (c : ℝ≥0∞)
    (hdom : c • Measure.map (fun ω => (1 / 2 : ℝ) • (X ω + Y ω)) ρ ≤ volume) :
    ∃ π : Measure (E d × E d), IsCoupling (uniformMeasure K) (uniformMeasure L) π ∧
      c • Measure.map (fun p : E d × E d => (1 / 2 : ℝ) • (p.1 + p.2)) π ≤ volume := by
…

    Mentions: OAI.Problem358.MidpointCoordinates.Coordinates, OAI.Problem358.MidpointCoordinates.coordinateUniform