Argmax.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.exists_measurable_finset_argmax line 15

Source documentation

A finite nonempty family of measurable scores has a measurable maximizing index. The maximizing score is measurable as well; no measurability assumption on individual index singletons is needed.

theorem exists_measurable_finset_argmax {X ι : Type*}
    [MeasurableSpace X] [MeasurableSpace ι]
    (f : ι → X → ℝ) (hf : ∀ i, Measurable (f i)) :
    ∀ (s : Finset ι), s.Nonempty →
      ∃ g : X → ι, Measurable g ∧ (∀ x, g x ∈ s) ∧
        Measurable (fun x => f (g x) x) ∧
        ∀ x i, i ∈ s → f i x ≤ f (g x) x := by
…

theorem OAI.Problem358.exists_measurable_argmax line 70

Source documentation

A measurable choice of an index maximizing a finite measurable family.

theorem exists_measurable_argmax {X ι : Type*}
    [MeasurableSpace X] [MeasurableSpace ι] [Fintype ι] [Nonempty ι]
    (f : ι → X → ℝ) (hf : ∀ i, Measurable (f i)) :
    ∃ g : X → ι, Measurable g ∧ Measurable (fun x => f (g x) x) ∧
      ∀ x i, f i x ≤ f (g x) x := by
…

theorem OAI.Problem358.exists_measurable_affine_maximizer line 82

Source documentation

Finite affine maxima have a globally measurable maximizing-slope map, including on their tie sets.

theorem exists_measurable_affine_maximizer {V ι : Type*}
    [NormedAddCommGroup V] [InnerProductSpace ℝ V]
    [MeasurableSpace V] [BorelSpace V]
    [Fintype ι] [Nonempty ι] (y : ι → V) (c : ι → ℝ) :
    ∃ T : V → V, Measurable T ∧ ∀ x, ∃ i,
      T x = y i ∧ ∀ j, ⟪y j, x⟫_ℝ + c j ≤ ⟪y i, x⟫_ℝ + c i := by
…

lemma OAI.Problem358.map_finite_selector line 108

Source documentation

The law of a finite choice of prescribed values is determined by the choice-cell masses.

lemma map_finite_selector {α β ι : Type*} [MeasurableSpace α] [MeasurableSpace β]
    [MeasurableSpace ι] [MeasurableSingletonClass ι] [Fintype ι]
    [MeasurableSingletonClass β] (ρ : Measure α) (s : α → ι)
    (hs : Measurable s) (y : ι → β) :
    Measure.map (fun x => y (s x)) ρ = ∑ i, ρ (s ⁻¹' {i}) • Measure.dirac (y i) := by
…

lemma OAI.Problem358.map_finite_selector_of_masses line 120

Source documentation

A version of map_finite_selector using supplied cell masses.

lemma map_finite_selector_of_masses {α β ι : Type*} [MeasurableSpace α] [MeasurableSpace β]
    [MeasurableSpace ι] [MeasurableSingletonClass ι] [Fintype ι]
    [MeasurableSingletonClass β] (ρ : Measure α) (s : α → ι)
    (hs : Measurable s) (y : ι → β) (w : ι → ℝ≥0∞)
    (hw : ∀ i, ρ (s ⁻¹' {i}) = w i) :
    Measure.map (fun x => y (s x)) ρ = ∑ i, w i • Measure.dirac (y i) := by
…

theorem OAI.Problem358.ParameterizedArgmax.ae_eq_of_maximizers line 140

Source documentation

Off the tie set, maximizing selectors are independent of every choice.

theorem ae_eq_of_maximizers
    {X ι : Type*} [MeasurableSpace X] (ρ : Measure X)
    (f : ι → X → ℝ) (k l : X → ι)
    (hsep : ∀ᵐ x ∂ρ, Function.Injective (fun i => f i x))
    (hk : ∀ᵐ x ∂ρ, ∀ i, f i x ≤ f (k x) x)
    (hl : ∀ᵐ x ∂ρ, ∀ i, f i x ≤ f (l x) x) : k =ᵐ[ρ] l := by
…

theorem OAI.Problem358.ParameterizedArgmax.exists_joint_measurable_argmax_with_masses line 152

Source documentation

Any pointwise family of prescribed-mass maximizing selectors can be replaced by one jointly measurable selector. Null ties preserve every mass exactly; no measurability of the original family of choices is assumed.

theorem exists_joint_measurable_argmax_with_masses
    {P X ι : Type*} [MeasurableSpace P] [MeasurableSpace X]
    [MeasurableSpace ι] [Fintype ι] [Nonempty ι]
    (ρ : P → Measure X) (f : ι → P × X → ℝ) (m : P → ι → ℝ)
    (hf : ∀ i, Measurable (f i))
    (hsep : ∀ p, ∀ᵐ x ∂ρ p, Function.Injective (fun i => f i (p, x)))
    (hex : ∀ p, ∃ k : X → ι,
      (∀ᵐ x ∂ρ p, ∀ i, f i (p, x) ≤ f (k x) (p, x)) ∧
      ∀ i, (ρ p).real {x | k x = i} = m p i) :
    ∃ k : P × X → ι, Measurable k ∧
      (∀ p x i, f i (p, x) ≤ f (k (p, x)) (p, x)) ∧
      ∀ p i, (ρ p).real {x | k (p, x) = i} = m p i := by
…

theorem OAI.Problem358.ParameterizedArgmax.exists_joint_measurable_affine_argmax_with_masses line 182

Source documentation

Concrete affine version for the uniform source: joint measurability of the sites/intercepts and injective sites discharge the score and null-tie premises.

theorem exists_joint_measurable_affine_argmax_with_masses
    {P ι : Type*} [MeasurableSpace P] [MeasurableSpace ι]
    [Fintype ι] [Nonempty ι] {d : ℕ} (K : Set (E d))
    (y : P → ι → E d) (c m : P → ι → ℝ)
    (hy : ∀ i, Measurable (fun p => y p i))
    (hc : ∀ i, Measurable (fun p => c p i))
    (hinj : ∀ p, Function.Injective (y p))
    (hex : ∀ p, ∃ k : E d → ι,
      (∀ᵐ x ∂uniformMeasure K, ∀ i,
        ⟪x, y p i⟫ + c p i ≤ ⟪x, y p (k x)⟫ + c p (k x)) ∧
      ∀ i, (uniformMeasure K).real {x | k x = i} = m p i) :
    ∃ k : P × E d → ι, Measurable k ∧
…