OAI/Analysis/Daugavet/ProductSeparation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactModuli.KW.near_additivity line 18

   Source documentation

   Near-disjointness from every old unit vector, using only the new scalar tail.

   lemma near_additivity {R : Type uR} [MeasurableSpace R] {ν : Measure R}
       [IsProbabilityMeasure ν] {w u : B → ℝ} {f : R → ℝ}
       (hw : Integrable w μ) (hu : Integrable u μ) (hf : Integrable f ν)
       (hfm : Measurable f) (hf0 : ∀ v, 0 ≤ f v)
       (hw1 : ∫ b, |w b| ∂μ = 1) (hu1 : ∫ b, |u b| ∂μ = 1)
       (hf1 : ∫ v, f v ∂ν = 1) {c : ℝ} (hc : 0 ≤ c) :
       2 - 2 * (ν.real {v | c < f v} + c) ≤
         ∫ z : B × R, |w z.1 + u z.1 * f z.2| ∂(μ.prod ν) := by
   …

2. def OAI.ExactModuli.KW.normalizeFunction line 69

   Source documentation

   Radial retraction to the old L1 unit ball, pointwise on representatives.

   def normalizeFunction (μ : Measure B) (f : B → ℝ) (b : B) : ℝ :=
   …

3. lemma OAI.ExactModuli.KW.integrable_normalizeFunction line 73
4. lemma OAI.ExactModuli.KW.normalizeFunction_bounds line 78
5. lemma OAI.ExactModuli.KW.restricted_markov line 117

   Source documentation

   Markov's inequality after discarding a small exceptional set.

   lemma restricted_markov {R : Type uR} [MeasurableSpace R] {ν : Measure R}
       [IsFiniteMeasure ν] {f b : R → ℝ} (hf : Integrable f ν) (hb : Integrable b ν)
       (hf0 : ∀ v, 0 ≤ f v) (hb0 : ∀ v, 0 ≤ b v)
       {D : Set R} (hD : MeasurableSet D) (hdom : ∀ v ∈ D, f v ≤ b v)
       {h : ℝ} (hh : 0 < h) :
       ν.real {v | h < f v} ≤ ν.real Dᶜ + (∫ v, b v ∂ν) / h := by
   …

   Mentions: OAI.ExactModuli.D

6. lemma OAI.ExactModuli.KW.old_norm_on_good_set line 146

   Source documentation

   Fubini on the good event controls the old approximant before normalization.

   lemma old_norm_on_good_set {R : Type uR} [MeasurableSpace R] {ν : Measure R}
       [IsProbabilityMeasure ν] {g : B × R → ℝ} {ψ U : B → ℝ}
       (hg : Integrable g (μ.prod ν)) (hψ : Integrable ψ μ) (hU : Integrable U μ)
       (_hU0 : ∀ b, 0 ≤ U b) {m r : ℝ} (hm : ∫ b, U b ∂μ = m) (_hr : 0 ≤ r)
       (hg1 : ∫ z, |g z| ∂(μ.prod ν) ≤ 1)
       {D : Set R} (hD : MeasurableSet D) (hDpos : 0 < ν.real D)
       (hgood : ∀ b v, v ∈ D → |g (b, v) - ψ b| ≤ r * U b) :
       (∫ b, |ψ b| ∂μ) ≤ r * m + 1 / ν.real D := by
   …

   Mentions: OAI.ExactModuli.D