Minimizers.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.normalized_intercept_lower_bound line 16

Source documentation

Positive weighted mean-zero coordinates bounded above are bounded below too.

theorem normalized_intercept_lower_bound
    (m c : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (hmean : ∑ i, m i * c i = 0) {R : ℝ} (hR : 0 ≤ R)
    (hupper : ∀ i, c i ≤ R) (i : ι) : -R / m i ≤ c i := by
…

theorem OAI.Problem358.exists_minimum_on_normalized_intercepts line 37

Source documentation

A continuous objective whose coordinate lower bounds control its sublevel sets attains a minimum on the positive weighted normalization hyperplane. This is the coercivity step in the prescribed-cell-mass variational argument.

theorem exists_minimum_on_normalized_intercepts
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (F : (ι → ℝ) → ℝ) (hF : Continuous F) (B : ℝ)
    (hlower : ∀ c : ι → ℝ, (∑ i, m i * c i) = 0 → ∀ i, c i - B ≤ F c) :
    ∃ c : ι → ℝ, (∑ i, m i * c i) = 0 ∧
      ∀ d : ι → ℝ, (∑ i, m i * d i) = 0 → F c ≤ F d := by
…

theorem OAI.Problem358.normalized_stationary_gradient_eq_zero line 71

Source documentation

The mass-residual gradient vanishes if it annihilates the normalization hyperplane and its unweighted coordinate sum is zero.

theorem normalized_stationary_gradient_eq_zero
    (m g : ι → ℝ) (hsum : ∑ i, m i = 1) (hgsum : ∑ i, g i = 0)
    (hstationary : ∀ q : ι → ℝ, (∑ i, m i * q i) = 0 →
      (∑ i, g i * q i) = 0) : g = 0 := by
…

theorem OAI.Problem358.gradient_eq_zero_of_normalized_minimum line 85

Source documentation

First-order optimality on the weighted normalization hyperplane, in a form directly applicable after differentiating the integral of a finite maximum.

theorem gradient_eq_zero_of_normalized_minimum
    (m g c : ι → ℝ) (hsum : ∑ i, m i = 1) (hgsum : ∑ i, g i = 0)
    (hc : ∑ i, m i * c i = 0) (F : (ι → ℝ) → ℝ)
    (hmin : ∀ d : ι → ℝ, (∑ i, m i * d i) = 0 → F c ≤ F d)
    (hderiv : ∀ q : ι → ℝ,
      HasDerivAt (fun t : ℝ => F (c + t • q)) (∑ i, g i * q i) 0) :
    g = 0 := by
…

theorem OAI.Problem358.exists_prescribed_masses_of_variational_objective line 110

Source documentation

Abstract prescribed-mass existence from a coercive potential objective and its cell-mass directional derivative. Geometry is isolated in hlower, hMsum, and hderiv; no existence or stationarity assumption is hidden in the conclusion.

theorem exists_prescribed_masses_of_variational_objective
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (F : (ι → ℝ) → ℝ) (hF : Continuous F) (B : ℝ)
    (hlower : ∀ c : ι → ℝ, (∑ i, m i * c i) = 0 → ∀ i, c i - B ≤ F c)
    (M : (ι → ℝ) → ι → ℝ) (hMsum : ∀ c, ∑ i, M c i = 1)
    (hderiv : ∀ c q : ι → ℝ,
      HasDerivAt (fun t : ℝ => F (c + t • q))
        (∑ i, (M c i - m i) * q i) 0) :
    ∃ c : ι → ℝ, (∑ i, m i * c i) = 0 ∧ M c = m := by
…

theorem OAI.Problem358.MaxPotential.abs_intercept_sub_le_of_active line 146

Source documentation

Every active affine branch has an intercept within twice the source-site product radius of every other active branch. No lower bound on the cell masses is needed.

theorem abs_intercept_sub_le_of_active
    (y : ι → V) (c : ι → ℝ) {R L : ℝ} (hL : 0 ≤ L)
    (hy : ∀ i, ‖y i‖ ≤ L)
    (hactive : ∀ i, ∃ x : V, ‖x‖ ≤ R ∧
      ∀ j, ⟪x, y j⟫ + c j ≤ ⟪x, y i⟫ + c i) :
    ∀ i j, |c i - c j| ≤ 2 * R * L := by
…

theorem OAI.Problem358.MaxPotential.abs_intercept_le_of_normalized line 168
Source documentation
Weighted normalization turns a bound on pairwise intercept differences into a bound on each intercept, without a reciprocal minimum-weight factor.
```
theorem abs_intercept_le_of_normalized
    (c m : ι → ℝ) {B : ℝ} (hm : ∀ i, 0 ≤ m i)
    (hsum : ∑ i, m i = 1) (hnormal : ∑ i, m i * c i = 0)
    (hspread : ∀ i j, |c i - c j| ≤ B) : ∀ i, |c i| ≤ B := by
…
```

theorem OAI.Problem358.MaxPotential.abs_intercept_sub_le_of_positive_cells line 189

Source documentation

Positive source mass in each maximizing cell gives the pointwise activity needed for the uniform intercept bound, even when maximality is only almost everywhere.

theorem abs_intercept_sub_le_of_positive_cells
    [MeasurableSpace V] (ρ : Measure V) (y : ι → V) (c : ι → ℝ)
    (k : V → ι) {R L : ℝ} (hL : 0 ≤ L) (hy : ∀ i, ‖y i‖ ≤ L)
    (hR : ∀ᵐ x ∂ρ, ‖x‖ ≤ R)
    (hmax : ∀ᵐ x ∂ρ, ∀ j, ⟪x, y j⟫ + c j ≤ ⟪x, y (k x)⟫ + c (k x))
    (hmass : ∀ i, 0 < ρ.real {x | k x = i}) :
    ∀ i j, |c i - c j| ≤ 2 * R * L := by
…

theorem OAI.Problem358.MaxPotential.abs_intercept_le_of_prescribed_cells line 211

Source documentation

A mass-normalized intercept solving the positive prescribed-cell problem lies in a fixed compact box determined only by the source and site radii.

theorem abs_intercept_le_of_prescribed_cells
    [MeasurableSpace V] (ρ : Measure V) (y : ι → V) (c m : ι → ℝ)
    (k : V → ι) {R L : ℝ} (hL : 0 ≤ L) (hy : ∀ i, ‖y i‖ ≤ L)
    (hR : ∀ᵐ x ∂ρ, ‖x‖ ≤ R)
    (hmax : ∀ᵐ x ∂ρ, ∀ j, ⟪x, y j⟫ + c j ≤ ⟪x, y (k x)⟫ + c (k x))
    (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (hnormal : ∑ i, m i * c i = 0)
    (hmass : ∀ i, ρ.real {x | k x = i} = m i) :
    ∀ i, |c i| ≤ 2 * R * L := by
…

def OAI.Problem358.MaxPotential.objective line 242
Source documentation
The finite-target variational objective as a function of affine intercepts.
```
def objective (y : ι → V) (m c : ι → ℝ) : ℝ :=
…
```
theorem OAI.Problem358.MaxPotential.continuous_objective line 245

theorem OAI.Problem358.MaxPotential.exists_minimum_objective line 254

Source documentation

The actual finite-potential objective attains its normalized minimum.

theorem exists_minimum_objective (y : ι → V) (m : ι → ℝ)
    (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1) (L : NNReal)
    (hy : ∀ i, ‖y i‖ ≤ L) (hρ : Integrable (fun x : V => ‖x‖) ρ) :
    ∃ c : ι → ℝ, (∑ i, m i * c i) = 0 ∧
      ∀ b : ι → ℝ, (∑ i, m i * b i) = 0 →
        objective ρ y m c ≤ objective ρ y m b := by
…

Mentions: OAI.Problem358.MaxPotential.objective

theorem OAI.Problem358.MaxPotential.exists_prescribed_masses line 270

Source documentation

A cell-mass derivative formula suffices to solve the prescribed mass problem. The only analytic input beyond integrability is the explicit directional derivative of the integral of the maximum; normalization and minimization are proved here.

theorem exists_prescribed_masses (y : ι → V) (m : ι → ℝ)
    (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1) (L : NNReal)
    (hy : ∀ i, ‖y i‖ ≤ L) (hρ : Integrable (fun x : V => ‖x‖) ρ)
    (M : (ι → ℝ) → ι → ℝ) (hMsum : ∀ c, ∑ i, M c i = 1)
    (hderiv : ∀ c q : ι → ℝ,
      HasDerivAt (fun t : ℝ => ∫ x, potential y (c + t • q) x ∂ρ)
        (∑ i, M c i * q i) 0) :
    ∃ c : ι → ℝ, (∑ i, m i * c i) = 0 ∧ M c = m := by
…

Mentions: OAI.Problem358.MaxPotential.potential

theorem OAI.Problem358.MaxPotential.minimizer_upper_bound line 319

Source documentation

A normalized potential minimizer has an explicit uniform coordinate upper bound.

theorem minimizer_upper_bound (ρ : Measure V) [IsProbabilityMeasure ρ]
    (y : ι → V) (c : ι → ℝ) (L : NNReal) (hy : ∀ i, ‖y i‖ ≤ L)
    (hρ : Integrable (fun x : V => ‖x‖) ρ)
    (hmin : (∫ x, potential y c x ∂ρ) ≤ ∫ x, potential y 0 x ∂ρ) :
    ∀ i, c i ≤ 2 * (L : ℝ) * ∫ x, ‖x‖ ∂ρ := by
…

Mentions: OAI.Problem358.MaxPotential.potential

theorem OAI.Problem358.MaxPotential.minimizer_mem_box line 338

Source documentation

The positive weighted normalization turns the preceding upper bound into a compact box.

theorem minimizer_mem_box (ρ : Measure V) [IsProbabilityMeasure ρ]
    (y : ι → V) (c m : ι → ℝ) (L : NNReal) (hy : ∀ i, ‖y i‖ ≤ L)
    (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1) (hc : ∑ i, m i * c i = 0)
    (hρ : Integrable (fun x : V => ‖x‖) ρ)
    (hmin : (∫ x, potential y c x ∂ρ) ≤ ∫ x, potential y 0 x ∂ρ) :
    c ∈ Set.Icc (fun i => -(2 * (L : ℝ) * ∫ x, ‖x‖ ∂ρ) / m i)
      (fun _ => 2 * (L : ℝ) * ∫ x, ‖x‖ ∂ρ) := by
…

Mentions: OAI.Problem358.MaxPotential.potential

theorem OAI.Problem358.MaxPotential.exists_prescribed_cell_masses line 369

Source documentation

Prescribed finite cell masses, with null affine ties as the only geometric input. The maximizing selector is globally measurable, including on exceptional tie sets.

theorem exists_prescribed_cell_masses (y : ι → V) (m : ι → ℝ)
    (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1) (L : NNReal)
    (hy : ∀ i, ‖y i‖ ≤ L) (hρ : Integrable (fun x : V => ‖x‖) ρ)
    (hties : ∀ c : ι → ℝ, ∀ᵐ x ∂ρ, ∀ i j, i ≠ j →
      ⟪x, y i⟫ + c i ≠ ⟪x, y j⟫ + c j) :
    ∃ (c : ι → ℝ) (k : V → ι),
      (∑ 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
…