MaxCalculus.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem358.FiniteMaxDerivative.maxValue line 15
Source documentation
The maximum of a nonempty finite family of real-valued functions.
```
def maxValue (f : ι → X → ℝ) (x : X) : ℝ :=
…
```
theorem OAI.Problem358.FiniteMaxDerivative.le_maxValue line 18
theorem OAI.Problem358.FiniteMaxDerivative.maxValue_le line 22

theorem OAI.Problem358.FiniteMaxDerivative.eventuallyEq_of_strict_max line 27

Source documentation

A strict active branch remains the maximum in a neighborhood.

theorem eventuallyEq_of_strict_max [TopologicalSpace X]
    {f : ι → X → ℝ} {x : X} {i : ι}
    (hc : ∀ j, ContinuousAt (f j) x)
    (hi : ∀ j, j ≠ i → f j x < f i x) :
    maxValue f =ᶠ[𝓝 x] f i := by
…

Mentions: OAI.Problem358.FiniteMaxDerivative.maxValue

theorem OAI.Problem358.FiniteMaxDerivative.hasDerivAt_of_strict_max line 42

Source documentation

Differentiation of a finite maximum at a strict active branch.

theorem hasDerivAt_of_strict_max {f : ι → ℝ → ℝ} {x f' : ℝ} {i : ι}
    (hc : ∀ j, ContinuousAt (f j) x)
    (hi : ∀ j, j ≠ i → f j x < f i x)
    (hd : HasDerivAt (f i) f' x) : HasDerivAt (maxValue f) f' x := by
…

Mentions: OAI.Problem358.FiniteMaxDerivative.maxValue

theorem OAI.Problem358.FiniteMaxDerivative.hasFDerivAt_of_strict_max line 49

Source documentation

The corresponding Fréchet derivative statement in any real normed space.

theorem hasFDerivAt_of_strict_max {V : Type*} [NormedAddCommGroup V]
    [NormedSpace ℝ V] {f : ι → V → ℝ} {x : V} {f' : V →L[ℝ] ℝ} {i : ι}
    (hc : ∀ j, ContinuousAt (f j) x)
    (hi : ∀ j, j ≠ i → f j x < f i x)
    (hd : HasFDerivAt (f i) f' x) : HasFDerivAt (maxValue f) f' x := by
…

Mentions: OAI.Problem358.FiniteMaxDerivative.maxValue

theorem OAI.Problem358.FiniteMaxDerivative.lipschitzWith_maxValue line 57
Source documentation
Taking a finite maximum preserves a common Lipschitz constant.
```
theorem lipschitzWith_maxValue [PseudoMetricSpace X]
    {f : ι → X → ℝ} {K : ℝ≥0} (hf : ∀ i, LipschitzWith K (f i)) :
    LipschitzWith K (maxValue f) := by
…
```
Mentions: OAI.Problem358.FiniteMaxDerivative.maxValue

theorem OAI.Problem358.FiniteMaxDerivative.lipschitzOnWith_maxValue line 68

Source documentation

The same bound holds on any common time domain.

theorem lipschitzOnWith_maxValue [PseudoMetricSpace X]
    {f : ι → X → ℝ} {K : ℝ≥0} {s : Set X}
    (hf : ∀ i, LipschitzOnWith K (f i) s) :
    LipschitzOnWith K (maxValue f) s := by
…

Mentions: OAI.Problem358.FiniteMaxDerivative.maxValue

theorem OAI.Problem358.FiniteMaxDerivative.exists_strict_max_of_injective line 84
Source documentation
A finite injective family of real scores has a strict maximizing index.
```
theorem exists_strict_max_of_injective (z : ι → ℝ) (hz : Function.Injective z) :
    ∃ i, ∀ j, j ≠ i → z j < z i := by
…
```

theorem OAI.Problem358.FiniteMaxDerivative.ae_ae_exists_strict_max line 94

Source documentation

Fubini moves the a.e. no-tie property from source sections to time sections.

theorem ae_ae_exists_strict_max {T Z : Type*} [MeasurableSpace T] [MeasurableSpace Z]
    {τ : Measure T} {ρ : Measure Z} [SFinite τ] [SFinite ρ]
    (f : ι → T × Z → ℝ) (hf : ∀ i, Measurable (f i))
    (hunique : ∀ᵐ t ∂τ, ∀ᵐ x ∂ρ, Function.Injective (fun i => f i (t, x))) :
    ∀ᵐ x ∂ρ, ∀ᵐ t ∂τ, ∃ i, ∀ j, j ≠ i → f j (t, x) < f i (t, x) := by
…

theorem OAI.Problem358.FiniteMaxDerivative.integral_deriv_maxValue line 120
Source documentation
Finite maxima of uniformly Lipschitz time branches obey the fundamental theorem.
```
theorem integral_deriv_maxValue {f : ι → ℝ → ℝ} {K : ℝ≥0} {a b : ℝ}
    (hf : ∀ i, LipschitzOnWith K (f i) (uIcc a b)) :
    ∫ t in a..b, deriv (maxValue f) t = maxValue f b - maxValue f a :=
…
```
Mentions: OAI.Problem358.FiniteMaxDerivative.maxValue

theorem OAI.Problem358.FiniteMaxDerivative.integral_eq_sub_of_ae_hasDerivAt line 126

Source documentation

Replace the derivative in the finite-max FTC by any a.e. derivative formula.

theorem integral_eq_sub_of_ae_hasDerivAt {f : ι → ℝ → ℝ} {K : ℝ≥0} {a b : ℝ}
    {v : ℝ → ℝ} (hf : ∀ i, LipschitzOnWith K (f i) (uIcc a b))
    (hv : ∀ᵐ t, t ∈ uIcc a b → HasDerivAt (maxValue f) (v t) t) :
    ∫ t in a..b, v t = maxValue f b - maxValue f a := by
…

Mentions: OAI.Problem358.FiniteMaxDerivative.maxValue

theorem OAI.Problem358.FiniteMaxDerivative.intervalIntegrable_of_ae_hasDerivAt line 136

Source documentation

An a.e. derivative formula for the finite maximum is interval integrable.

theorem intervalIntegrable_of_ae_hasDerivAt {f : ι → ℝ → ℝ} {K : ℝ≥0}
    {a b : ℝ} {v : ℝ → ℝ}
    (hf : ∀ i, LipschitzOnWith K (f i) (uIcc a b))
    (hv : ∀ᵐ t, t ∈ uIcc a b → HasDerivAt (maxValue f) (v t) t) :
    IntervalIntegrable v volume a b := by
…

Mentions: OAI.Problem358.FiniteMaxDerivative.maxValue

theorem OAI.Problem358.FiniteMaxDerivative.integral_active_deriv_eq_sub line 146

Source documentation

The FTC identity with the derivative of an a.e. strict active branch.

theorem integral_active_deriv_eq_sub {f f' : ι → ℝ → ℝ} {K : ℝ≥0}
    {a b : ℝ} (active : ℝ → ι)
    (hf : ∀ i, LipschitzOnWith K (f i) (uIcc a b))
    (hd : ∀ᵐ t, t ∈ uIcc a b → ∀ j, HasDerivAt (f j) (f' j t) t)
    (hstrict : ∀ᵐ t, t ∈ uIcc a b → ∀ j, j ≠ active t →
      f j t < f (active t) t) :
    ∫ t in a..b, f' (active t) t = maxValue f b - maxValue f a := by
…

Mentions: OAI.Problem358.FiniteMaxDerivative.maxValue

theorem OAI.Problem358.FiniteMaxDerivative.hasDerivAt_affine_max line 163

Source documentation

The time derivative of a finite affine potential on a strict active cell.

theorem hasDerivAt_affine_max {y : ι → ℝ → V} {c : ι → ℝ → ℝ}
    {v : ι → V} {r : ι → ℝ} {t : ℝ} {i : ι} (x : V)
    (hy : ∀ j, HasDerivAt (y j) (v j) t)
    (hc : ∀ j, HasDerivAt (c j) (r j) t)
    (hi : ∀ j, j ≠ i → inner ℝ x (y j t) + c j t <
      inner ℝ x (y i t) + c i t) :
    HasDerivAt (maxValue (fun j s => inner ℝ x (y j s) + c j s))
      (inner ℝ x (v i) + r i) t := by
…

Mentions: OAI.Problem358.FiniteMaxDerivative.maxValue

theorem OAI.Problem358.FiniteMaxDerivative.lipschitzOnWith_affine_max_of_deriv_bounds line 179

Source documentation

Uniform bounds on site and intercept speeds make the potential Lipschitz in time.

theorem lipschitzOnWith_affine_max_of_deriv_bounds
    {y : ι → ℝ → V} {c : ι → ℝ → ℝ} {v : ι → ℝ → V} {r : ι → ℝ → ℝ}
    {s : Set ℝ} (hs : Convex ℝ s) (x : V) {R A B : ℝ≥0}
    (hx : ‖x‖ ≤ R)
    (hy : ∀ j t, t ∈ s → HasDerivAt (y j) (v j t) t)
    (hc : ∀ j t, t ∈ s → HasDerivAt (c j) (r j t) t)
    (hv : ∀ j t, t ∈ s → ‖v j t‖ ≤ A)
    (hr : ∀ j t, t ∈ s → ‖r j t‖ ≤ B) :
    LipschitzOnWith (R * A + B)
      (maxValue (fun j t => inner ℝ x (y j t) + c j t)) s := by
…

Mentions: OAI.Problem358.FiniteMaxDerivative.maxValue

def OAI.Problem358.FiniteMaxDerivative.finiteMax line 221
Source documentation
The maximum of a nonempty finite family of real numbers.
```
def finiteMax (f : ι → ℝ) : ℝ :=
…
```
lemma OAI.Problem358.FiniteMaxDerivative.le_finiteMax line 224
lemma OAI.Problem358.FiniteMaxDerivative.finiteMax_le line 227
lemma OAI.Problem358.FiniteMaxDerivative.finiteMax_eq line 230
lemma OAI.Problem358.FiniteMaxDerivative.eventually_finiteMax_eq line 234
Source documentation
A strict maximizer remains the maximizer for a sufficiently small affine perturbation.
```
lemma eventually_finiteMax_eq (f q : ι → ℝ) (i : ι)
    (hi : ∀ j, j ≠ i → f j < f i) :
    (fun t : ℝ => finiteMax (fun j => f j + t * q j)) =ᶠ[𝓝 0]
      (fun t => f i + t * q i) := by
…
```
Mentions: OAI.Problem358.FiniteMaxDerivative.finiteMax
lemma OAI.Problem358.FiniteMaxDerivative.hasDerivAt_finiteMax line 250
Source documentation
Directional derivative of a finite maximum at a strict maximizer.
```
lemma hasDerivAt_finiteMax (f q : ι → ℝ) (i : ι)
    (hi : ∀ j, j ≠ i → f j < f i) :
    HasDerivAt (fun t : ℝ => finiteMax (fun j => f j + t * q j)) (q i) 0 := by
…
```
Mentions: OAI.Problem358.FiniteMaxDerivative.finiteMax
lemma OAI.Problem358.FiniteMaxDerivative.lipschitzWith_finiteMax line 258
Source documentation
The maximum is uniformly Lipschitz in an affine parameter, independently of offsets.
```
lemma lipschitzWith_finiteMax (f q : ι → ℝ) (B : ℝ≥0)
    (hq : ∀ i, |q i| ≤ B) :
    LipschitzWith B (fun t : ℝ => finiteMax (fun i => f i + t * q i)) := by
…
```
Mentions: OAI.Problem358.FiniteMaxDerivative.finiteMax
lemma OAI.Problem358.FiniteMaxDerivative.aestronglyMeasurable_finiteMax line 279

lemma OAI.Problem358.FiniteMaxDerivative.integrable_finite_selection line 291

Source documentation

Every finite-valued measurable selection is integrable for a finite measure.

lemma integrable_finite_selection {ι : Type*} [Fintype ι] [Nonempty ι]
    {α : Type*} [MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ]
    (q : ι → ℝ) (k : α → ι)
    (hk : ∀ i, MeasurableSet {x | k x = i}) :
    Integrable (fun x => q (k x)) μ := by
…

lemma OAI.Problem358.FiniteMaxDerivative.integral_finite_selection line 305

Source documentation

Integrate a finite-valued selection by summing its fiber masses.

lemma integral_finite_selection {ι : Type*} [Fintype ι] [Nonempty ι]
    {α : Type*} [MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ]
    (q : ι → ℝ) (k : α → ι)
    (hk : ∀ i, MeasurableSet {x | k x = i}) :
    (∫ x, q (k x) ∂μ) = ∑ i, μ.real {x | k x = i} * q i := by
…

lemma OAI.Problem358.FiniteMaxDerivative.sum_cellMass_eq_one line 326
Source documentation
The masses of a finite measurable partition sum to one under a probability measure.
```
lemma sum_cellMass_eq_one [IsProbabilityMeasure μ] (k : α → ι)
    (hk : ∀ i, MeasurableSet {x | k x = i}) :
    (∑ i, μ.real {x | k x = i}) = 1 := by
…
```

theorem OAI.Problem358.FiniteMaxDerivative.hasDerivAt_integral_finiteMax line 333

Source documentation

Differentiate an integral of finite maxima when its active index is unique almost everywhere. The Lipschitz bound is independent of the point and hence integrable for every finite measure.

theorem hasDerivAt_integral_finiteMax [IsFiniteMeasure μ]
    (f : ι → α → ℝ) (q : ι → ℝ) (k : α → ι)
    (hf : ∀ i, AEStronglyMeasurable (f i) μ)
    (hint : Integrable (fun x => finiteMax (fun i => f i x)) μ)
    (hk : ∀ᵐ x ∂μ, ∀ j, j ≠ k x → f j x < f (k x) x)
    (hqk : AEStronglyMeasurable (fun x => q (k x)) μ) :
    HasDerivAt (fun t : ℝ => ∫ x, finiteMax (fun i => f i x + t * q i) ∂μ)
      (∫ x, q (k x) ∂μ) 0 := by
…

Mentions: OAI.Problem358.FiniteMaxDerivative.finiteMax

theorem OAI.Problem358.FiniteMaxDerivative.hasDerivAt_integral_finiteMax_cellMass line 365

Source documentation

Cell-mass form of the derivative formula, with only measurable fibers required of the index.

theorem hasDerivAt_integral_finiteMax_cellMass [IsFiniteMeasure μ]
    (f : ι → α → ℝ) (q : ι → ℝ) (k : α → ι)
    (hf : ∀ i, AEStronglyMeasurable (f i) μ)
    (hint : Integrable (fun x => finiteMax (fun i => f i x)) μ)
    (hk : ∀ᵐ x ∂μ, ∀ j, j ≠ k x → f j x < f (k x) x)
    (hkmeas : ∀ i, MeasurableSet {x | k x = i}) :
    HasDerivAt (fun t : ℝ => ∫ x, finiteMax (fun i => f i x + t * q i) ∂μ)
      (∑ i, μ.real {x | k x = i} * q i) 0 := by
…

Mentions: OAI.Problem358.FiniteMaxDerivative.finiteMax

theorem OAI.Problem358.FiniteMaxDerivative.hasDerivAt_intercept_objective line 378

Source documentation

Directional derivative of the finite-cell intercept objective.

theorem hasDerivAt_intercept_objective [IsFiniteMeasure μ]
    (f : ι → α → ℝ) (c q m : ι → ℝ) (k : α → ι)
    (hf : ∀ i, AEStronglyMeasurable (f i) μ)
    (hint : Integrable (fun x => finiteMax (fun i => f i x + c i)) μ)
    (hk : ∀ᵐ x ∂μ, ∀ j, j ≠ k x → f j x + c j < f (k x) x + c (k x))
    (hkmeas : ∀ i, MeasurableSet {x | k x = i}) :
    HasDerivAt
      (fun t : ℝ => (∫ x, finiteMax (fun i => f i x + (c i + t * q i)) ∂μ) -
        ∑ i, m i * (c i + t * q i))
      (∑ i, (μ.real {x | k x = i} - m i) * q i) 0 := by
…

Mentions: OAI.Problem358.FiniteMaxDerivative.finiteMax

theorem OAI.Problem358.ae_prod_injective_affine_scores line 415

Source documentation

Injective moving affine slopes have jointly almost-everywhere distinct scores. The joint conclusion is what is needed to integrate derivatives along time paths.

theorem ae_prod_injective_affine_scores (K : Set (E d))
    {τ : Measure ℝ} [SFinite (uniformMeasure K)]
    {y : ι → ℝ → E d} {c : ι → ℝ → ℝ}
    (hy : ∀ i, Measurable (y i)) (hc : ∀ i, Measurable (c i))
    (hinj : ∀ᵐ t ∂τ, Function.Injective (fun i => y i t)) :
    ∀ᵐ p ∂τ.prod (uniformMeasure K),
      Function.Injective (fun i => ⟪p.2, y i p.1⟫_ℝ + c i p.1) := by
…

theorem OAI.Problem358.ae_prod_strict_active_affine line 448

Source documentation

Any maximizing selector of moving affine scores is strictly active jointly a.e. when the moving slopes are a.e. injective.

theorem ae_prod_strict_active_affine (K : Set (E d))
    {τ : Measure ℝ} [SFinite (uniformMeasure K)]
    {y : ι → ℝ → E d} {c : ι → ℝ → ℝ}
    (active : ℝ → E d → ι)
    (hy : ∀ i, Measurable (y i)) (hc : ∀ i, Measurable (c i))
    (hinj : ∀ᵐ t ∂τ, Function.Injective (fun i => y i t))
    (hactive : ∀ᵐ p ∂τ.prod (uniformMeasure K), ∀ j,
      ⟪p.2, y j p.1⟫_ℝ + c j p.1 ≤
        ⟪p.2, y (active p.1 p.2) p.1⟫_ℝ + c (active p.1 p.2) p.1) :
    ∀ᵐ p ∂τ.prod (uniformMeasure K), ∀ j, j ≠ active p.1 p.2 →
      ⟪p.2, y j p.1⟫_ℝ + c j p.1 <
        ⟪p.2, y (active p.1 p.2) p.1⟫_ℝ + c (active p.1 p.2) p.1 := by
…

theorem OAI.Problem358.ae_prod_hasDerivAt_affine_max line 467

Source documentation

The time derivative of a moving finite affine maximum agrees jointly a.e. with the affine velocity on any maximizing selector. Thus no separate no-ties or strict-cell hypothesis is needed for the fundamental-theorem step.

theorem ae_prod_hasDerivAt_affine_max [Nonempty ι] (K : Set (E d))
    {τ : Measure ℝ} [SFinite (uniformMeasure K)]
    {y v : ι → ℝ → E d} {c r : ι → ℝ → ℝ}
    (active : ℝ → E d → ι)
    (hy : ∀ i, Measurable (y i)) (hc : ∀ i, Measurable (c i))
    (hinj : ∀ᵐ t ∂τ, Function.Injective (fun i => y i t))
    (hdy : ∀ᵐ t ∂τ, ∀ j, HasDerivAt (y j) (v j t) t)
    (hdc : ∀ᵐ t ∂τ, ∀ j, HasDerivAt (c j) (r j t) t)
    (hactive : ∀ᵐ p ∂τ.prod (uniformMeasure K), ∀ j,
      ⟪p.2, y j p.1⟫_ℝ + c j p.1 ≤
        ⟪p.2, y (active p.1 p.2) p.1⟫_ℝ + c (active p.1 p.2) p.1) :
    ∀ᵐ p ∂τ.prod (uniformMeasure K),
…