bounded_bochner_mean_quadratic_transport_control

Plain-English statement

Actual Bochner means controlled by the infimum of quadratic costs over all actual couplings, with cost finiteness and residual norm bounds produced. No optimizer or cost-minimizer assumption. Fresh independent source and compiler audits accepted. Final root/reader gates and postmerge purification remain separate; no whole-model or convergence credit.

Lean statement

theorem bounded_bochner_mean_quadratic_transport_control
    {U H : Type*} [MeasurableSpace U]
    [NormedAddCommGroup H] [NormedSpace ℝ H] [CompleteSpace H]
    (K : U → H) (hK : StronglyMeasurable K)
    (B C L : ℝ) (hB : 0 ≤ B) (hC : 0 ≤ C) (hL : 0 ≤ L)
    (hBound : ∀ u, ‖K u‖ ≤ B)
    (c : U × U → ℝ) (hc : Measurable c)
    (hc0 : ∀ z, 0 ≤ c z) (hcBound : ∀ z, c z ≤ C)
    (hLip : ∀ u v, ‖K u-K v‖ ≤ L * c (u,v))
    (μ ν : Measure U) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] :
    let cost : U × U → ℝ≥0∞ := fun z => ENNReal.ofReal ((c z)^2)
    let Q := AutoSamplingTheory.TechnicalLemmas.Measure.Transport.transportCost cost μ ν
    let W := Q ^ (1 / 2 : ℝ)
    Integrable K μ ∧ Integrable K ν ∧ Q ≠ ∞ ∧
      ‖(∫ u, K u ∂μ) - (∫ v, K v ∂ν)‖ ≤ L * W.toReal ∧
      ∀ y : H, ‖(∫ u, K u ∂μ)-y‖ ≤ B+‖y‖ ∧
        ‖(∫ v, K v ∂ν)-y‖ ≤ B+‖y‖ := by
  dsimp only
  let cost : U × U → ℝ≥0∞ := fun z => ENNReal.ofReal ((c z)^2)
  let Q := AutoSamplingTheory.TechnicalLemmas.Measure.Transport.transportCost cost μ ν
  have hQ : Q ≠ ∞ := actual_transport_cost_finite c C hC hc0 hcBound μ ν
  have hμ : Integrable K μ := bounded_feature_integrable K hK B hBound μ
  have hν : Integrable K ν := bounded_feature_integrable K hK B hBound ν
  have hs (γ : Measure (U × U))
      (hγ : AutoSamplingTheory.TechnicalLemmas.Measure.Transport.IsCoupling γ μ ν) :
      ‖(∫ u, K u ∂μ)-(∫ v, K v ∂ν)‖^2 ≤ L^2 * ∫ z, (c z)^2 ∂γ :=
    actual_coupling_squared_mean_bound K hK B C L hC hL hBound c hc hc0 hcBound hLip μ ν γ hγ
  refine ⟨hμ,hν,hQ,?_,?_⟩
  · let A := ‖(∫ u, K u ∂μ)-(∫ v, K v ∂ν)‖
    change A ≤ L * (Q ^ (1 / 2 : ℝ)).toReal
    by_cases hL0 : L = 0
    · have h := hs (μ.prod ν)
        (AutoSamplingTheory.TechnicalLemmas.Measure.Transport.isCoupling_prod μ ν)
      rw [hL0] at *
      simp only [zero_mul,zero_pow (by decide : 2 ≠ 0)] at *
      change A^2 ≤ 0 at h
      nlinarith [norm_nonneg ((∫ u, K u ∂μ)-(∫ v, K v ∂ν))]
    · have hLp : 0 < L := lt_of_le_of_ne hL (Ne.symm hL0)
      have hLow : ENNReal.ofReal ((A/L)^2) ≤ Q := by
        apply le_sInf
        rintro q ⟨γ,hγ,rfl⟩
        letI : IsProbabilityMeasure γ :=
          AutoSamplingTheory.TechnicalLemmas.Measure.Transport.isProbabilityMeasure_of_isCoupling_left hγ
        have hcLp : MemLp c 2 γ := (memLp_const C).mono' hc.aestronglyMeasurable
          (ae_of_all _ fun z => by simpa only [Real.norm_of_nonneg (hc0 z)] using hcBound z)
        have hcSq : Integrable (fun z => (c z)^2) γ := (memLp_two_iff_integrable_sq hcLp.1).1 hcLp
        change ENNReal.ofReal ((A/L)^2) ≤ ∫⁻ z, ENNReal.ofReal ((c z)^2) ∂γ
        rw [← ofReal_integral_eq_lintegral_ofReal hcSq (ae_of_all _ fun z => sq_nonneg _)]
        apply ENNReal.ofReal_le_ofReal
        rw [div_pow]
        apply (div_le_iff₀ (sq_pos_of_pos hLp)).2
        simpa only [mul_comm] using hs γ hγ
      have hReal := ENNReal.toReal_mono hQ hLow
      rw [ENNReal.toReal_ofReal (sq_nonneg _)] at hReal
      have he : (Q ^ (1 / 2 : ℝ))^2 = Q := by
        rw [← ENNReal.rpow_two,← ENNReal.rpow_mul]
        norm_num
      have heReal : ((Q ^ (1 / 2 : ℝ)).toReal)^2 = Q.toReal := by
        rw [← ENNReal.toReal_pow,he]
      have hr : A/L ≤ (Q ^ (1 / 2 : ℝ)).toReal := by
        have ha : 0 ≤ A/L := div_nonneg (norm_nonneg _) hL
        have hb := ENNReal.toReal_nonneg (a := Q ^ (1 / 2 : ℝ))
        nlinarith
      calc
        A = L * (A/L) := by field_simp
        _ ≤ L * (Q ^ (1 / 2 : ℝ)).toReal := mul_le_mul_of_nonneg_left hr hL
  · have hmμ : ‖∫ u, K u ∂μ‖ ≤ B := by
      simpa only [probReal_univ,mul_one] using
        (norm_integral_le_of_norm_le_const (μ := μ) (ae_of_all _ hBound))
    have hmν : ‖∫ v, K v ∂ν‖ ≤ B := by
      simpa only [probReal_univ,mul_one] using
        (norm_integral_le_of_norm_le_const (μ := ν) (ae_of_all _ hBound))
    intro y
    exact ⟨(norm_sub_le _ _).trans (add_le_add hmμ le_rfl),
      (norm_sub_le _ _).trans (add_le_add hmν le_rfl)⟩

end AutoSamplingTheory.TechnicalLemmas.Measure.BochnerMeanTransport

Open AutoSamplingTheory/TechnicalLemmas/Measure/BochnerMeanTransport.lean:129published source at ed709a7f320d

Proof architecture

Generic probability, optimisation and sphere-feature prerequisites; concrete model compositions remain separate

Lean proof walkthrough

• Read the quantified variables and typeclass brackets as part of the mathematical statement; inferred arguments are not missing assumptions.
• `intro` introduces quantified hypotheses into the local proof context.
• `have` creates a named intermediate mathematical fact.
• `calc` records an equality or inequality chain matching a paper calculation.
• `rw` rewrites by an established identity.
• `simp` normalizes through registered definitional and theorem rewrites.
• `apply` reduces the goal to the hypotheses of a reusable theorem.
• `refine` instantiates a reusable theorem while leaving explicit subgoals.

Why the statement has this shape

The declaration is kept at the reusable level recorded by its Registry tags and direct consumers. Explicit measures, spaces, wrappers, and regularity hypotheses expose interfaces that paper notation often infers. A theorem card explains those interfaces but never widens the compiled statement.

Hidden assumptions and non-claims

• Measurability is represented explicitly or must be supplied by a dependency.
• Integrability is an input or proved output; a displayed integral alone does not supply it.
• Almost-everywhere hypotheses depend on the stated measure and representative.