OAI/Analysis/Brenier/InterceptEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem358.CellGeometry.stationary_face_moment_estimate line 18

    Source documentation

    The stationary moment estimate in the face-coordinate form required by the mass-Jacobian argument. The two derivative hypotheses are ordinary derivatives of the actual closed-cell integrals, not quantitative inequalities.

    theorem stationary_face_moment_estimate
    {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
    {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
    (hKi : (interior K).Nonempty) (y : ι → E d) (c q : ι → ℝ)
    (hy : Function.Injective y) (R : ℝ) (hR : 0 ≤ R)
    (hbounded : ∀ᵐ x ∂uniformMeasure K, ‖x‖ ≤ R)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i)
    (hmass : ∀ i, (uniformMeasure K).real (closedCell K y c i) = m i)
    (g : ι → ι → ℝ) (b : ι → ι → E d)
    (hB : ∀ i, HasDerivAt
      (fun s : ℝ => ∫ x in closedCell K y (fun j => c j + s * q j) i,
        x ∂uniformMeasure K) (∑ j, (q i - q j) • b i j) 0)
…

    Mentions: OAI.Problem358.CellGeometry.closedCell

  2. theorem OAI.Problem358.CellGeometry.fixed_mass_intercept_energy_of_convex_midpoint line 53

    Source documentation

    Actual cell derivatives and convex-body midpoint couplings supply the full weighted intercept-energy estimate. No moment inequality or inverse-Jacobian estimate is assumed: the stationary estimate and connected range argument are both invoked internally.

    theorem fixed_mass_intercept_energy_of_convex_midpoint
    {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
    {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
    (hKi : (interior K).Nonempty) (y : ι → E d) (c : ι → ℝ)
    (hy : Function.Injective y) (R : ℝ) (hR : 0 ≤ R)
    (hbounded : ∀ᵐ x ∂uniformMeasure K, ‖x‖ ≤ R)
    (m r : ι → ℝ) (v : ι → E d) {w : ℝ}
    (hm : ∀ i, 0 < m i)
    (hmass : ∀ i, (uniformMeasure K).real (closedCell K y c i) = m i)
    (g : ι → ι → ℝ) (b : ι → ι → E d)
    (hg : ∀ i j, g i j = g j i) (hb : ∀ i j, b i j = b j i)
    (hg0 : ∀ i j, 0 ≤ g i j) (G : SimpleGraph ι)
…

    Mentions: OAI.Problem358.CellGeometry.closedCell

  3. theorem OAI.Problem358.FixedMassIntercepts.intercepts_comp_deriv_energy_le_of_convex_midpoint line 105

    Source documentation

    The canonical prescribed-mass intercept path has the required uniform weighted derivative energy. All branch existence, uniqueness, differentiability, normalization and fixed-mass differentiation are supplied internally. The remaining inputs are the actual geometric mass/moment differentials and the convex-body midpoint coupling.

    theorem intercepts_comp_deriv_energy_le_of_convex_midpoint
    {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
    [MeasurableSpace ι] [MeasurableSingletonClass ι]
    {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
    (hKi : (interior K).Nonempty)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (Y : ℝ → (ι → E d)) (v : ι → E d) (t : ℝ)
    (hY : HasDerivAt Y v t) (hy : Function.Injective (Y t))
    (R : ℝ) (hR : 0 ≤ R) {w : ℝ}
    (hbounded : ∀ᵐ x ∂uniformMeasure K, ‖x‖ ≤ R)
    (g : ι → ι → ℝ) (b : ι → ι → E d)
    (hg : ∀ i j, g i j = g j i) (hb : ∀ i j, b i j = b j i)
…
  4. theorem OAI.Problem358.CellGeometry.normalizedMassMap_derivative_apply line 173

    Source documentation

    Any Fréchet derivative of the actual normalized mass map has the canonical geometric formula. This follows by uniqueness from the proved line derivative; it is independent of how the bounded linear operator was constructed.

    theorem normalizedMassMap_derivative_apply
    {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
    {ρ : Measure (E d)} (hρ : ρ ≪ volume)
    {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
    (m : ι → ℝ) (y : ι → E d) (c : CellLaplacian.normalizedSpace m)
    (hy : Function.Injective y) (hpos : ∀ i, ρ (closedCell K y c i) ≠ 0)
    (A : ((ι → E d) × CellLaplacian.normalizedSpace m) →L[ℝ] (ι → ℝ))
    (hD : HasFDerivAt (normalizedMassMap K m) A (y, c))
    (v : ι → E d) (q : CellLaplacian.normalizedSpace m) :
    A (v, q) = CellLaplacian.apply (PositiveFacet.canonicalFaceWeight K y c) q +
      CellLaplacian.siteFlux (faceMoment K y c) v := by
…

    Mentions: OAI.Problem358.CellLaplacian.normalizedSpace, OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.CellGeometry.normalizedMassMap, OAI.Problem358.CellLaplacian.apply, OAI.Problem358.PositiveFacet.canonicalFaceWeight, OAI.Problem358.CellLaplacian.siteFlux, OAI.Problem358.CellGeometry.faceMoment

  5. theorem OAI.Problem358.FixedMassIntercepts.contDiffAt_intercepts_of_normalizedMassC1 line 202

    Source documentation

    Genuine C¹ regularity of the normalized mass map implies C¹ regularity of the canonical prescribed-mass choice. The geometric derivative and connected Laplacian are identified internally, independently of any operator API.

    theorem contDiffAt_intercepts_of_normalizedMassC1
    {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
    [MeasurableSpace ι] [MeasurableSingletonClass ι]
    {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
    (hKi : (interior K).Nonempty)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (y : ι → E d) (hy : Function.Injective y)
    (hC1 : ContDiffAt ℝ 1 (CellGeometry.normalizedMassMap K m)
      (y, intercepts hK hconv hKi m hm hsum y)) :
    ContDiffAt ℝ 1 (intercepts hK hconv hKi m hm hsum) y := by
…

    Mentions: OAI.Problem358.CellGeometry.normalizedMassMap, OAI.Problem358.FixedMassIntercepts.intercepts

  6. theorem OAI.Problem358.FixedMassIntercepts.intercepts_comp_deriv_energy_le_of_massC1_convex_midpoint line 241

    Source documentation

    Pointwise derivative energy for the actual canonical intercepts, with every face, graph, mass and moment differential supplied by the geometry. Only C¹ regularity of the actual normalized mass map and the convex midpoint coupling remain as analytic inputs. No operator formula or chosen-branch hypothesis is assumed.

    theorem intercepts_comp_deriv_energy_le_of_massC1_convex_midpoint
    {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
    [MeasurableSpace ι] [MeasurableSingletonClass ι]
    {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
    (hKi : (interior K).Nonempty)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (Y : ℝ → (ι → E d)) (v : ι → E d) (t : ℝ)
    (hY : HasDerivAt Y v t) (hy : Function.Injective (Y t))
    (R : ℝ) (hR : 0 ≤ R) {w : ℝ}
    (hbounded : ∀ᵐ x ∂uniformMeasure K, ‖x‖ ≤ R)
    (hspeed : (∑ i, m i * ‖v i‖ ^ 2) ≤ w ^ 2)
    (hC1 : ContDiffAt ℝ 1 (CellGeometry.normalizedMassMap K m)
…

    Mentions: OAI.Problem358.CellGeometry.normalizedMassMap