PrescribedCells.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.MaxPotential.exists_prescribed_cell_masses_of_ac_volume line 17

Source documentation

An absolutely continuous probability with finite first moment realizes every strictly positive finite mass vector by an affine maximum partition.

theorem exists_prescribed_cell_masses_of_ac_volume
    (ρ : Measure (E d)) [IsProbabilityMeasure ρ]
    (hac : ρ ≪ (volume : Measure (E d)))
    (hρ : Integrable (fun x : E d => ‖x‖) ρ)
    (y : ι → E d) (hinj : Function.Injective y) (m : ι → ℝ)
    (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1) :
    ∃ (c : ι → ℝ) (k : E d → ι),
      (∑ i, m i * c i) = 0 ∧ Measurable k ∧
      (∀ x j, ⟪x, y j⟫ + c j ≤ ⟪x, y (k x)⟫ + c (k x)) ∧
      (∀ i, ρ.real {x | k x = i} = m i) := by
…

theorem OAI.Problem358.MaxPotential.exists_prescribed_cell_masses_uniform line 41

Source documentation

The prescribed-mass affine partition exists for the uniform source on a compact body. Compactness supplies the first moment; no cell calculus is assumed.

theorem exists_prescribed_cell_masses_uniform
    (K : Set (E d)) [IsProbabilityMeasure (uniformMeasure K)]
    (hK : IsCompact K) (y : ι → E d) (hinj : Function.Injective y) (m : ι → ℝ)
    (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1) :
    ∃ (c : ι → ℝ) (k : E d → ι),
      (∑ i, m i * c i) = 0 ∧ Measurable k ∧
      (∀ x j, ⟪x, y j⟫ + c j ≤ ⟪x, y (k x)⟫ + c (k x)) ∧
      (∀ i, (uniformMeasure K).real {x | k x = i} = m i) := by
…

theorem OAI.Problem358.MaxPotential.integral_subgradient_of_cell_masses line 76

Source documentation

Prescribed cell masses yield the supporting inequality for the integrated potential. This is the elementary subgradient argument, with no differentiation.

theorem integral_subgradient_of_cell_masses (ρ : Measure V) [IsFiniteMeasure ρ]
    (y : ι → V) (c a m : ι → ℝ) (k : V → ι)
    (hk : ∀ i, MeasurableSet {x | k x = i})
    (hmax : ∀ᵐ x ∂ρ, ∀ j, ⟪x, y j⟫ + c j ≤ ⟪x, y (k x)⟫ + c (k x))
    (hmass : ∀ i, ρ.real {x | k x = i} = m i)
    (hc : Integrable (potential y c) ρ) (ha : Integrable (potential y a) ρ) :
    (∫ x, potential y c x ∂ρ) + (∑ i, m i * (a i - c i)) ≤
      ∫ x, potential y a x ∂ρ := by
…

Mentions: OAI.Problem358.MaxPotential.potential

theorem OAI.Problem358.MaxPotential.isMin_of_cell_masses line 96

Source documentation

Every normalized prescribed-mass solution minimizes the normalized objective.

theorem isMin_of_cell_masses (ρ : Measure V) [IsFiniteMeasure ρ]
    (y : ι → V) (c m : ι → ℝ) (k : V → ι)
    (hc0 : ∑ i, m i * c i = 0)
    (hk : ∀ i, MeasurableSet {x | k x = i})
    (hmax : ∀ᵐ x ∂ρ, ∀ j, ⟪x, y j⟫ + c j ≤ ⟪x, y (k x)⟫ + c (k x))
    (hmass : ∀ i, ρ.real {x | k x = i} = m i)
    (hint : ∀ a : ι → ℝ, Integrable (potential y a) ρ) :
    ∀ a : ι → ℝ, (∑ i, m i * a i) = 0 →
      (∫ x, potential y c x ∂ρ) ≤ ∫ x, potential y a x ∂ρ := by
…

Mentions: OAI.Problem358.MaxPotential.potential

theorem OAI.Problem358.MaxPotential.prescribed_cell_masses_unique line 111

Source documentation

Prescribed positive masses determine normalized intercepts uniquely for a connected full-support source. Only affine null ties, not cell calculus, are needed.

theorem prescribed_cell_masses_unique (ρ : Measure V) [IsFiniteMeasure ρ] {K : Set V}
    (hK : IsPreconnected K) (hKs : K ⊆ ρ.support) (hKae : ∀ᵐ x ∂ρ, x ∈ K)
    (y : ι → V) (c b m : ι → ℝ) (k l : V → ι)
    (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (hc0 : ∑ i, m i * c i = 0) (hb0 : ∑ i, m i * b i = 0)
    (hk : ∀ i, MeasurableSet {x | k x = i})
    (hl : ∀ i, MeasurableSet {x | l x = i})
    (hmaxc : ∀ᵐ x ∂ρ, ∀ j, ⟪x, y j⟫ + c j ≤ ⟪x, y (k x)⟫ + c (k x))
    (hmaxb : ∀ᵐ x ∂ρ, ∀ j, ⟪x, y j⟫ + b j ≤ ⟪x, y (l x)⟫ + b (l x))
    (hmassc : ∀ i, ρ.real {x | k x = i} = m i)
    (hmassb : ∀ i, ρ.real {x | l x = i} = m i)
    (hties : ∀ᵐ x ∂ρ, ∀ i j, i ≠ j →
…

theorem OAI.Problem358.CellGeometry.abs_intercept_sub_le_of_nonempty_closedCells line 153
Source documentation
On a source contained in a radius-R ball, intercept differences of nonempty cells are controlled by the distance between their sites. This does not require distinct sites, measurable selectors, or a lower mass bound.
```
theorem abs_intercept_sub_le_of_nonempty_closedCells
    {K : Set (E d)} (y : ι → E d) (c : ι → ℝ) {R : ℝ}
    (hR : ∀ x ∈ K, ‖x‖ ≤ R)
    (hne : ∀ i, (closedCell K y c i).Nonempty) :
    ∀ i j, |c i - c j| ≤ R * ‖y i - y j‖ := by
…
```
Mentions: OAI.Problem358.CellGeometry.closedCell

theorem OAI.Problem358.CellGeometry.abs_intercept_sub_le_of_positive_closedCells line 177

Source documentation

The preceding estimate applies directly to positive real closed-cell masses, independently of any argmax selection.

theorem abs_intercept_sub_le_of_positive_closedCells
    {K : Set (E d)} (ρ : Measure (E d)) (y : ι → E d) (c : ι → ℝ)
    {R : ℝ} (hR : ∀ x ∈ K, ‖x‖ ≤ R)
    (hpos : ∀ i, 0 < ρ.real (closedCell K y c i)) :
    ∀ i j, |c i - c j| ≤ R * ‖y i - y j‖ := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell

theorem OAI.Problem358.CellGeometry.abs_intercept_le_of_normalized_closedCells line 191

Source documentation

Weighted normalization yields a mass-independent compact box for the actual closed-cell intercept problem. Only nonemptiness of each cell is used.

theorem abs_intercept_le_of_normalized_closedCells [Fintype ι]
    {K : Set (E d)} (y : ι → E d) (c m : ι → ℝ) {R L : ℝ}
    (hR : ∀ x ∈ K, ‖x‖ ≤ R) (hL : 0 ≤ L) (hy : ∀ i, ‖y i‖ ≤ L)
    (hne : ∀ i, (closedCell K y c i).Nonempty)
    (hm : ∀ i, 0 ≤ m i) (hsum : ∑ i, m i = 1)
    (hnormal : ∑ i, m i * c i = 0) :
    ∀ i, |c i| ≤ 2 * R * L := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell

theorem OAI.Problem358.CellGeometry.abs_intercept_le_of_prescribed_closedCells line 206

Source documentation

A direct quantitative consequence of prescribed positive closed-cell masses and normalization, in the spelling used by the actual mass map.

theorem abs_intercept_le_of_prescribed_closedCells [Fintype ι]
    {K : Set (E d)} (ρ : Measure (E d)) (y : ι → E d) (c m : ι → ℝ)
    {R L : ℝ} (hR : ∀ x ∈ K, ‖x‖ ≤ R) (hL : 0 ≤ L)
    (hy : ∀ i, ‖y i‖ ≤ L) (hm : ∀ i, 0 < m i)
    (hsum : ∑ i, m i = 1) (hnormal : ∑ i, m i * c i = 0)
    (hmass : ∀ i, ρ.real (closedCell K y c i) = m i) :
    ∀ i, |c i| ≤ 2 * R * L := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell

theorem OAI.Problem358.CellGeometry.abs_intercept_sub_le_of_closedCell_limit line 224

Source documentation

The geometric spread estimate survives coefficient limits, even if sites collide and individual closed-cell masses cease to be continuous.

theorem abs_intercept_sub_le_of_closedCell_limit
    {A : Type*} {l : Filter A} [NeBot l] {K : Set (E d)}
    (y : A → ι → E d) (c : A → ι → ℝ) (y₀ : ι → E d) (c₀ : ι → ℝ)
    {R : ℝ} (hR : ∀ x ∈ K, ‖x‖ ≤ R)
    (hne : ∀ᶠ t in l, ∀ i, (closedCell K (y t) (c t) i).Nonempty)
    (hy : ∀ i, Tendsto (fun t => y t i) l (𝓝 (y₀ i)))
    (hc : ∀ i, Tendsto (fun t => c t i) l (𝓝 (c₀ i))) :
    ∀ i j, |c₀ i - c₀ j| ≤ R * ‖y₀ i - y₀ j‖ := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell

theorem OAI.Problem358.CellGeometry.intercept_eq_of_eq_site_of_closedCell_limit line 241

Source documentation

In a limit of nonempty fixed-source cells, colliding sites necessarily have equal intercepts. Endpoint coalescence therefore needs no choice of a largest intercept among these repeated slopes.

theorem intercept_eq_of_eq_site_of_closedCell_limit
    {A : Type*} {l : Filter A} [NeBot l] {K : Set (E d)}
    (y : A → ι → E d) (c : A → ι → ℝ) (y₀ : ι → E d) (c₀ : ι → ℝ)
    {R : ℝ} (hR : ∀ x ∈ K, ‖x‖ ≤ R)
    (hne : ∀ᶠ t in l, ∀ i, (closedCell K (y t) (c t) i).Nonempty)
    (hy : ∀ i, Tendsto (fun t => y t i) l (𝓝 (y₀ i)))
    (hc : ∀ i, Tendsto (fun t => c t i) l (𝓝 (c₀ i)))
    {i j : ι} (hij : y₀ i = y₀ j) : c₀ i = c₀ j := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell

theorem OAI.Problem358.MaxPotential.uniform_prescribed_cell_masses_unique line 266

Source documentation

On a compact convex body, positive prescribed masses and weighted normalization uniquely determine the intercepts of distinct affine sites.

theorem uniform_prescribed_cell_masses_unique {d : ℕ} {K : Set (E d)}
    (hK : IsCompact K) (hconv : Convex ℝ K) (hne : (interior K).Nonempty)
    (y : ι → E d) (hy : Function.Injective y) (c b m : ι → ℝ) (k l : E d → ι)
    (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (hc0 : ∑ i, m i * c i = 0) (hb0 : ∑ i, m i * b i = 0)
    (hk : ∀ i, MeasurableSet {x | k x = i})
    (hl : ∀ i, MeasurableSet {x | l x = i})
    (hmaxc : ∀ᵐ x ∂uniformMeasure K, ∀ j,
      ⟪x, y j⟫ + c j ≤ ⟪x, y (k x)⟫ + c (k x))
    (hmaxb : ∀ᵐ x ∂uniformMeasure K, ∀ j,
      ⟪x, y j⟫ + b j ≤ ⟪x, y (l x)⟫ + b (l x))
    (hmassc : ∀ i, (uniformMeasure K).real {x | k x = i} = m i)
…

theorem OAI.Problem358.MaxPotential.uniform_normalized_minimizer_unique line 297

Source documentation

For distinct sites and positive normalized weights the normalized uniform-source variational objective has at most one minimizer. All geometric hypotheses are concrete.

theorem uniform_normalized_minimizer_unique {d : ℕ} {K : Set (E d)}
    (hK : IsCompact K) (hconv : Convex ℝ K) (hne : (interior K).Nonempty)
    (y : ι → E d) (hy : Function.Injective y) (m : ι → ℝ)
    (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (c b : ι → ℝ) (hc0 : ∑ i, m i * c i = 0) (hb0 : ∑ i, m i * b i = 0)
    (hcmin : ∀ a : ι → ℝ, (∑ i, m i * a i) = 0 →
      (∫ x, potential y c x ∂uniformMeasure K) ≤ ∫ x, potential y a x ∂uniformMeasure K)
    (hbmin : ∀ a : ι → ℝ, (∑ i, m i * a i) = 0 →
      (∫ x, potential y b x ∂uniformMeasure K) ≤ ∫ x, potential y a x ∂uniformMeasure K) :
    c = b := by
…

Mentions: OAI.Problem358.MaxPotential.potential