OAI/Analysis/Brenier/PotentialTime.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem358.PotentialTimeIntegral.sq_integral_le_mass_mul_integral_sq line 11

   Source documentation

   Cauchy--Schwarz against the constant function, without real powers.

   theorem sq_integral_le_mass_mul_integral_sq
       {T : Type*} [MeasurableSpace T] {ν : Measure T} [IsFiniteMeasure ν]
       {f : T → ℝ} (hmass : 0 < ν.real univ) (hf : Integrable f ν)
       (hf2 : Integrable (fun t => f t ^ 2) ν) :
       (∫ t, f t ∂ν) ^ 2 ≤ ν.real univ * ∫ t, f t ^ 2 ∂ν := by
   …

2. theorem OAI.Problem358.PotentialTimeIntegral.integral_sq_of_time_integral_le line 39

   Source documentation

   Spatial squared L² control for a pointwise time-integral representation.

   theorem integral_sq_of_time_integral_le
       {T X : Type*} [MeasurableSpace T] [MeasurableSpace X]
       {ν : Measure T} {μ : Measure X} [IsFiniteMeasure ν] [SFinite μ]
       {v : T → X → ℝ} {F : X → ℝ}
       (hmass : 0 < ν.real univ)
       (hv : Integrable (Function.uncurry v) (ν.prod μ))
       (hv2 : Integrable (fun p : T × X => v p.1 p.2 ^ 2) (ν.prod μ))
       (hF2 : Integrable (fun x => F x ^ 2) μ)
       (hF : ∀ᵐ x ∂μ, F x = ∫ t, v t x ∂ν) :
       (∫ x, F x ^ 2 ∂μ) ≤
         ν.real univ * ∫ t, ∫ x, v t x ^ 2 ∂μ ∂ν := by
   …

3. theorem OAI.Problem358.PotentialTimeIntegral.sqrt_integral_sq_of_time_integral_le line 61

   Source documentation

   A uniform spatial L² speed bound integrates to a spatial L² displacement bound.

   theorem sqrt_integral_sq_of_time_integral_le
       {T X : Type*} [MeasurableSpace T] [MeasurableSpace X]
       {ν : Measure T} {μ : Measure X} [IsFiniteMeasure ν] [SFinite μ]
       {v : T → X → ℝ} {F : X → ℝ} {B : ℝ}
       (hmass : 0 < ν.real univ) (hB : 0 ≤ B)
       (hv : Integrable (Function.uncurry v) (ν.prod μ))
       (hv2 : Integrable (fun p : T × X => v p.1 p.2 ^ 2) (ν.prod μ))
       (hF2 : Integrable (fun x => F x ^ 2) μ)
       (hF : ∀ᵐ x ∂μ, F x = ∫ t, v t x ∂ν)
       (hspeed : ∀ᵐ t ∂ν, (∫ x, v t x ^ 2 ∂μ) ≤ B ^ 2) :
       Real.sqrt (∫ x, F x ^ 2 ∂μ) ≤ ν.real univ * B := by
   …

4. theorem OAI.Problem358.PotentialTimeIntegral.potential_path_L2_bound line 86

   Source documentation

   The time-interval form of the potential-path estimate, with an a.e. FTC identity.

   theorem potential_path_L2_bound
       {X : Type*} [MeasurableSpace X] {μ : Measure X} [SFinite μ]
       {u v : ℝ → X → ℝ} {s t B : ℝ} (hst : s < t) (hB : 0 ≤ B)
       (hv : Integrable (Function.uncurry v) ((volume.restrict (Ioc s t)).prod μ))
       (hv2 : Integrable (fun p : ℝ × X => v p.1 p.2 ^ 2)
         ((volume.restrict (Ioc s t)).prod μ))
       (hu2 : Integrable (fun x => (u t x - u s x) ^ 2) μ)
       (hFTC : ∀ᵐ x ∂μ, u t x - u s x = ∫ r in s..t, v r x)
       (hspeed : ∀ᵐ r ∂volume.restrict (Ioc s t), (∫ x, v r x ^ 2 ∂μ) ≤ B ^ 2) :
       Real.sqrt (∫ x, (u t x - u s x) ^ 2 ∂μ) ≤ B * (t - s) := by
   …

5. theorem OAI.Problem358.PotentialTimeIntegral.potential_path_L2_bound_of_absolutelyContinuous line 106

   Source documentation

   The path estimate with FTC supplied by absolute continuity and an a.e. derivative. The derivative hypothesis is joint in time and space, as in the finite-max construction.

   theorem potential_path_L2_bound_of_absolutelyContinuous
       {X : Type*} [MeasurableSpace X] {μ : Measure X} [SFinite μ]
       {u v : ℝ → X → ℝ} {s t B : ℝ} (hst : s < t) (hB : 0 ≤ B)
       (hv : Integrable (Function.uncurry v) ((volume.restrict (Ioc s t)).prod μ))
       (hv2 : Integrable (fun p : ℝ × X => v p.1 p.2 ^ 2)
         ((volume.restrict (Ioc s t)).prod μ))
       (hu2 : Integrable (fun x => (u t x - u s x) ^ 2) μ)
       (hu : ∀ᵐ x ∂μ, AbsolutelyContinuousOnInterval (fun r => u r x) s t)
       (hderiv : ∀ᵐ p ∂(volume.restrict (Ioc s t)).prod μ,
         HasDerivAt (fun r => u r p.2) (v p.1 p.2) p.1)
       (hspeed : ∀ᵐ r ∂volume.restrict (Ioc s t), (∫ x, v r x ^ 2 ∂μ) ≤ B ^ 2) :
       Real.sqrt (∫ x, (u t x - u s x) ^ 2 ∂μ) ≤ B * (t - s) := by
   …

6. theorem OAI.Problem358.PotentialTimeIntegral.potential_path_L2_bound_of_lipschitz line 133

   Source documentation

   A locally uniform Lipschitz bound in time is enough for the preceding theorem.

   theorem potential_path_L2_bound_of_lipschitz
       {X : Type*} [MeasurableSpace X] {μ : Measure X} [SFinite μ]
       {u v : ℝ → X → ℝ} {s t B : ℝ} (hst : s < t) (hB : 0 ≤ B)
       (hv : Integrable (Function.uncurry v) ((volume.restrict (Ioc s t)).prod μ))
       (hv2 : Integrable (fun p : ℝ × X => v p.1 p.2 ^ 2)
         ((volume.restrict (Ioc s t)).prod μ))
       (hu2 : Integrable (fun x => (u t x - u s x) ^ 2) μ)
       (hu : ∀ᵐ x ∂μ, ∃ L : ℝ≥0, LipschitzOnWith L (fun r => u r x) (Icc s t))
       (hderiv : ∀ᵐ p ∂(volume.restrict (Ioc s t)).prod μ,
         HasDerivAt (fun r => u r p.2) (v p.1 p.2) p.1)
       (hspeed : ∀ᵐ r ∂volume.restrict (Ioc s t), (∫ x, v r x ^ 2 ∂μ) ≤ B ^ 2) :
       Real.sqrt (∫ x, (u t x - u s x) ^ 2 ∂μ) ≤ B * (t - s) := by
   …

7. theorem OAI.Problem358.PotentialSpeed.integral_selector line 162

   Source documentation

   Integration over a finite measurable selector is the weighted sum over its fibers.

   theorem integral_selector {X I : Type*} [MeasurableSpace X]
       [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I]
       {μ : Measure X} [IsFiniteMeasure μ] {sel : X → I} (hsel : Measurable sel)
       (f : I → ℝ) :
       (∫ x, f (sel x) ∂μ) = ∑ i, μ.real {x | sel x = i} * f i := by
   …

8. theorem OAI.Problem358.PotentialSpeed.integrable_selector line 176

   Source documentation

   Every real-valued finite-selector function is integrable on a finite measure.

   theorem integrable_selector {X I : Type*} [MeasurableSpace X]
       [Finite I] [MeasurableSpace I] [MeasurableSingletonClass I]
       {μ : Measure X} [IsFiniteMeasure μ] {sel : X → I} (hsel : Measurable sel)
       (f : I → ℝ) : Integrable (fun x => f (sel x)) μ := by
   …

9. theorem OAI.Problem358.PotentialSpeed.affine_sq_le line 183

   Source documentation

   A pointwise speed bound with a harmless factor of two.

   theorem affine_sq_le {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
       {x v : H} {r R : ℝ} (hx : ‖x‖ ≤ R) :
       (inner ℝ x v + r) ^ 2 ≤ 2 * R ^ 2 * ‖v‖ ^ 2 + 2 * r ^ 2 := by
   …

10. theorem OAI.Problem358.PotentialSpeed.integral_affine_speed_sq_le line 196

    Source documentation

    Weighted cellwise integration of the time derivative of a finite affine maximum.

    theorem integral_affine_speed_sq_le
        {H I : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
        [MeasurableSpace H] [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I]
        {μ : Measure H} [IsFiniteMeasure μ] {sel : H → I} (hsel : Measurable sel)
        (v : I → H) (r : I → ℝ) {R : ℝ}
        (hR : ∀ᵐ x ∂μ, ‖x‖ ≤ R)
        (hint : Integrable (fun x => (inner ℝ x (v (sel x)) + r (sel x)) ^ 2) μ) :
        (∫ x, (inner ℝ x (v (sel x)) + r (sel x)) ^ 2 ∂μ) ≤
          2 * R ^ 2 * (∑ i, μ.real {x | sel x = i} * ‖v i‖ ^ 2) +
            2 * (∑ i, μ.real {x | sel x = i} * r i ^ 2) := by
    …

11. theorem OAI.Problem358.PotentialSpeed.integrable_affine_speed_sq line 225

    Source documentation

    A bounded source and a measurable finite selector give the required square integrability.

    theorem integrable_affine_speed_sq
        {H I : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
        [MeasurableSpace H] [OpensMeasurableSpace H] [SecondCountableTopology H]
        [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I]
        {μ : Measure H} [IsFiniteMeasure μ] {sel : H → I} (hsel : Measurable sel)
        (v : I → H) (r : I → ℝ) {R : ℝ} (hR : ∀ᵐ x ∂μ, ‖x‖ ≤ R) :
        Integrable (fun x => (inner ℝ x (v (sel x)) + r (sel x)) ^ 2) μ := by
    …

12. theorem OAI.Problem358.PotentialSpeed.integral_affine_speed_sq_le_of_energy line 243

    Source documentation

    From the coupling and intercept energy bounds to the spatial potential speed bound. The constant is non-sharp, which is sufficient for one-third stability.

    theorem integral_affine_speed_sq_le_of_energy
        {H I : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
        [MeasurableSpace H] [OpensMeasurableSpace H] [SecondCountableTopology H]
        [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I]
        {μ : Measure H} [IsFiniteMeasure μ] {sel : H → I} (hsel : Measurable sel)
        (v : I → H) (r m : I → ℝ) {R w k : ℝ}
        (hR : ∀ᵐ x ∂μ, ‖x‖ ≤ R)
        (hm : ∀ i, μ.real {x | sel x = i} = m i)
        (hv : (∑ i, m i * ‖v i‖ ^ 2) ≤ w ^ 2)
        (hr : (∑ i, m i * r i ^ 2) ≤ k * R ^ 2 * w ^ 2) :
        (∫ x, (inner ℝ x (v (sel x)) + r (sel x)) ^ 2 ∂μ) ≤
          2 * (1 + k) * R ^ 2 * w ^ 2 := by
    …

13. theorem OAI.Problem358.FiniteMaxDerivative.measurable_selected line 281

    Source documentation

    Selecting a measurable member of a finite measurable family stays measurable.

    theorem measurable_selected (g : ι → X → ℝ) (k : X → ι)
        (hg : ∀ i, Measurable (g i)) (hk : ∀ i, MeasurableSet {x | k x = i}) :
        Measurable (fun x => g (k x) x) := by
    …

14. theorem OAI.Problem358.FiniteMaxDerivative.measurable_maxValue line 292

    Source documentation

    Endpoint values of the finite maximum are measurable.

    theorem measurable_maxValue (f : ι → X → ℝ) (hf : ∀ i, Measurable (f i)) :
        Measurable (maxValue f) := by
    …

    Mentions: OAI.Problem358.FiniteMaxDerivative.maxValue

15. theorem OAI.Problem358.FiniteMaxDerivative.finite_max_path_L2_bound line 304

    Source documentation

    A finite maximum inherits the spatial L² time bound from its active-branch speed. All integrability and pointwise FTC obligations are discharged by measurability and uniform bounds.

    theorem finite_max_path_L2_bound
        {μ : Measure X} [IsFiniteMeasure μ] {a b B D : ℝ} {L : ℝ≥0}
        (f g : ι → ℝ × X → ℝ) (k : ℝ × X → ι)
        (hab : a < b) (hB : 0 ≤ B)
        (hf : ∀ i, Measurable (f i)) (hg : ∀ i, Measurable (g i))
        (hk : ∀ i, MeasurableSet {p | k p = i})
        (hLip : ∀ᵐ x ∂μ, ∀ i, LipschitzOnWith L (fun r => f i (r, x)) (Icc a b))
        (hderiv : ∀ᵐ p ∂(volume.restrict (Ioc a b)).prod μ, ∀ i,
          HasDerivAt (fun r => f i (r, p.2)) (g i p) p.1)
        (hstrict : ∀ᵐ p ∂(volume.restrict (Ioc a b)).prod μ, ∀ j, j ≠ k p →
          f j p < f (k p) p)
        (hbound : ∀ᵐ p ∂(volume.restrict (Ioc a b)).prod μ, ‖g (k p) p‖ ≤ D)
    …

16. theorem OAI.Problem358.finite_potential_path_bound line 366

    Source documentation

    Quantitative potential-path estimate from fixed cell masses, the coupling energy, and the intercept energy. This is the time-integration step of finite-target stability.

    theorem finite_potential_path_bound
        {H I : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
        [MeasurableSpace H] [OpensMeasurableSpace H] [SecondCountableTopology H]
        [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I]
        {μ : Measure H} [IsFiniteMeasure μ]
        (u : ℝ → H → ℝ) (sel : ℝ → H → I) (v : I → H) (r : ℝ → I → ℝ) (m : I → ℝ)
        {s t R w k : ℝ} (hst : s < t) (hR : 0 ≤ R) (hw : 0 ≤ w) (hk : 0 ≤ k)
        (hxR : ∀ᵐ x ∂μ, ‖x‖ ≤ R)
        (hsel : ∀ q ∈ Ioc s t, Measurable (sel q))
        (hm : ∀ q ∈ Ioc s t, ∀ i, μ.real {x | sel q x = i} = m i)
        (hvEnergy : (∑ i, m i * ‖v i‖ ^ 2) ≤ w ^ 2)
        (hrEnergy : ∀ q ∈ Ioc s t, (∑ i, m i * r q i ^ 2) ≤ k * R ^ 2 * w ^ 2)
    …