production module

`AutoSamplingTheory.TechnicalLemmas.Measure.ReplacementCompetitorQuadraticCost`

3 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Measure/ReplacementCompetitorQuadraticCost.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.PermutedReplacementQuadraticCostAutoSamplingTheory.TechnicalLemmas.Measure.ReplacementCompetitorMathlib.MeasureTheory.Integral.Bochner.Basic external

Imported by

AutoSamplingTheory.TechnicalLemmas.Measure.QuadraticOptimalSupportCyclicTests.ReplacementCompetitorQuadraticCost

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

theorem AutoSamplingTheory.TechnicalLemmas.Measure.ReplacementCompetitorQuadraticCost.integrable_ambient_of_remainder_removed Partial Not mapped

- Integrability of the unchanged remainder and removed block implies integrability of the reconstructed ambient measure.

theorem integrable_ambient_of_remainder_removed
    (ambient remainder removed : FiniteMeasure (E × E))
    (hdecomp : ambient = remainder + removed)
    (hrem : Integrable realQuadraticCost (remainder : Measure (E × E)))
    (hremoved : Integrable realQuadraticCost (removed : Measure (E × E))) :
    Integrable realQuadraticCost (ambient : Measure (E × E)) := by
  rw [hdecomp]
  exact integrable_add_measure.2 ⟨hrem, hremoved⟩

/-- Integrability of the unchanged remainder and replacement block implies
integrability of the global replacement competitor. -/

AutoSamplingTheory/TechnicalLemmas/Measure/ReplacementCompetitorQuadraticCost.lean:30published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.ReplacementCompetitorQuadraticCost.integrable_replacementCompetitor Partial Not mapped

- Integrability of the unchanged remainder and replacement block implies integrability of the global replacement competitor.

theorem integrable_replacementCompetitor
    (remainder replacement : FiniteMeasure (E × E))
    (hrem : Integrable realQuadraticCost (remainder : Measure (E × E)))
    (hreplacement : Integrable realQuadraticCost (replacement : Measure (E × E))) :
    Integrable realQuadraticCost
      (replacementCompetitor remainder replacement : Measure (E × E)) := by
  unfold replacementCompetitor
  exact integrable_add_measure.2 ⟨hrem, hreplacement⟩

/-- A strict cost improvement on the removed/replacement part remains strict
after the same remainder is added to both sides. -/

AutoSamplingTheory/TechnicalLemmas/Measure/ReplacementCompetitorQuadraticCost.lean:41published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.ReplacementCompetitorQuadraticCost.integral_replacementCompetitor_lt_ambient Partial Not mapped

- A strict cost improvement on the removed/replacement part remains strict after the same remainder is added to both sides.

theorem integral_replacementCompetitor_lt_ambient
    (ambient remainder removed replacement : FiniteMeasure (E × E))
    (hdecomp : ambient = remainder + removed)
    (hrem : Integrable realQuadraticCost (remainder : Measure (E × E)))
    (hremoved : Integrable realQuadraticCost (removed : Measure (E × E)))
    (hreplacement : Integrable realQuadraticCost (replacement : Measure (E × E)))
    (hcost :
      (∫ z, realQuadraticCost z ∂(replacement : Measure (E × E))) <
        ∫ z, realQuadraticCost z ∂(removed : Measure (E × E))) :
    (∫ z, realQuadraticCost z
        ∂(replacementCompetitor remainder replacement : Measure (E × E))) <
      ∫ z, realQuadraticCost z ∂(ambient : Measure (E × E)) := by
  calc
    (∫ z, realQuadraticCost z
        ∂(replacementCompetitor remainder replacement : Measure (E × E))) =
        (∫ z, realQuadraticCost z ∂(remainder : Measure (E × E))) +
          ∫ z, realQuadraticCost z ∂(replacement : Measure (E × E)) := by
      unfold replacementCompetitor
      exact integral_add_measure hrem hreplacement
    _ < (∫ z, realQuadraticCost z ∂(remainder : Measure (E × E))) +
        ∫ z, realQuadraticCost z ∂(removed : Measure (E × E)) :=
      add_lt_add_left hcost _
    _ = ∫ z, realQuadraticCost z
        ∂((remainder + removed : FiniteMeasure (E × E)) : Measure (E × E)) := by
      exact (integral_add_measure hrem hremoved).symm
    _ = ∫ z, realQuadraticCost z ∂(ambient : Measure (E × E)) := by
      rw [← hdecomp]

end

end ReplacementCompetitorQuadraticCost
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/ReplacementCompetitorQuadraticCost.lean:52published source at 0e31a3cda412