import PhysicsLogic.Papers.Onsager1931

open PhysicsLogic.Papers.Onsager1931 MeasureTheory

namespace FunctionalContract
open DissipationFunctional
variable {Flow : Type} [AddCommGroup Flow] [Module Real Flow]

example (data : Data Flow) : data.ReciprocalAt =
    (∀ first second, data.resistancePairing first second = data.resistancePairing second first) := rfl
example (data : Data Flow) (flow : Flow) : data.dissipation flow =
    data.resistancePairing flow flow / 2 := rfl
example (data : Data Flow) (flow : Flow) : data.functional flow =
    data.entropySupply flow - data.dissipation flow := rfl
example (data : Data Flow) : data.NonnegativeDissipationAt =
    (∀ flow, 0 ≤ data.dissipation flow) := rfl
example (data : Data Flow) : data.StrictDissipationAt =
    (∀ flow, flow ≠ 0 → 0 < data.dissipation flow) := rfl
example (data : Data Flow) (physical : Flow) : data.ConstitutiveAt physical =
    (∀ variation, data.entropySupply variation = data.resistancePairing variation physical) := rfl
example (data : Data Flow) (physical : Flow) : data.MaximumAt physical =
    (∀ trial, data.functional trial ≤ data.functional physical) := rfl
example (data : Data Flow) (physical : Flow) : data.UniqueMaximumAt physical =
    (∀ trial, trial ≠ physical → data.functional trial < data.functional physical) := rfl
example (data : Data Flow) (physical : Flow) : data.NonvacuousDissipationMaximumAt physical =
    (physical ≠ 0 ∧ 0 < data.dissipation physical ∧ data.ConstitutiveAt physical ∧
      data.MaximumAt physical ∧ data.UniqueMaximumAt physical ∧
        data.entropySupply physical = 2 * data.dissipation physical) := rfl
example (temperature : Real) (resistance : Matrix (Fin 2) (Fin 2) Real) (force : Fin 2 → Real) :
    (Data.ofResistance temperature resistance force).resistancePairing =
      temperature⁻¹ • Matrix.toBilin' resistance := rfl
example (temperature : Real) (resistance : Matrix (Fin 2) (Fin 2) Real) (force : Fin 2 → Real) :
    (Data.ofResistance temperature resistance force).entropySupply =
      temperature⁻¹ • Matrix.toBilin' (1 : Matrix (Fin 2) (Fin 2) Real) force := rfl
example : Countermodels.reciprocal = Data.ofResistance 2 !![2, 1; 1, 2] ![4, 5] := rfl
example : Countermodels.physical = (![1, 2] : Fin 2 → Real) := rfl
example : Countermodels.skew = Data.ofResistance 1 !![1, 1; -1, 1] ![1, -1] := rfl
example : Countermodels.skewPhysical = (![1, 0] : Fin 2 → Real) := rfl
example : Countermodels.degenerate = Data.ofResistance 2 !![2, 0; 0, 0] ![2, 0] := rfl
example : Countermodels.degeneratePhysical = (![1, 0] : Fin 2 → Real) := rfl
end FunctionalContract

namespace SpatialContract
variable {Flow : Type} [AddCommGroup Flow] [Module Real Flow]

example (readout : HeatDissipationReadout Flow) (position : HeatPosition) (axis : Fin 3) :
    readout.inverseTemperatureGradientAt position axis =
      deriv (fun step : Real =>
        (readout.temperatureValueAt (position + step • (Pi.single axis (1 : Real) : HeatPosition)))⁻¹) 0 := rfl
example (readout : HeatDissipationReadout Flow) (flow : Flow) (position : HeatPosition) :
    readout.divergenceAt flow position =
      ∑ axis : Fin 3, deriv (fun step : Real =>
        readout.flowValueAt flow (position + step • (Pi.single axis (1 : Real) : HeatPosition)) axis) 0 := rfl
example (readout : HeatDissipationReadout Flow) (flow : Flow) (position : HeatPosition) :
    readout.normalFluxAt flow position =
      ∑ axis, readout.outwardNormalAt position axis * readout.flowValueAt flow position axis := rfl
example (readout : HeatDissipationReadout Flow) (flow : Flow) : readout.systemEntropyRate flow =
    ∫ position, -readout.divergenceAt flow position / readout.temperatureValueAt position
      ∂readout.volumeMeasure := rfl
example (readout : HeatDissipationReadout Flow) (flow : Flow) : readout.boundaryEntropyRate flow =
    ∫ position, readout.normalFluxAt flow position / readout.temperatureValueAt position
      ∂readout.boundaryMeasure := rfl
example (readout : HeatDissipationReadout Flow) (first second : Flow) (position : HeatPosition) :
    readout.resistancePairingDensityAt first second position =
      (∑ firstAxis, ∑ secondAxis,
        readout.flowValueAt first position firstAxis * readout.resistanceValueAt position firstAxis secondAxis *
          readout.flowValueAt second position secondAxis) / readout.temperatureValueAt position := rfl
example (readout : HeatDissipationReadout Flow) (flow : Flow) (position : HeatPosition) :
    readout.entropySupplyDensityAt flow position =
      ∑ axis, readout.flowValueAt flow position axis * readout.inverseTemperatureGradientAt position axis := rfl
example (readout : HeatDissipationReadout Flow) : readout.PositiveTemperatureAt =
    (∀ position, 0 < readout.temperatureValueAt position) := rfl
example (readout : HeatDissipationReadout Flow) : readout.DifferentiabilityDomainAt =
    (∀ position axis,
      DifferentiableAt Real (fun step : Real =>
        readout.temperatureValueAt (position + step • (Pi.single axis (1 : Real) : HeatPosition))) 0 ∧
      ∀ flow, DifferentiableAt Real (fun step : Real =>
        readout.flowValueAt flow (position + step • (Pi.single axis (1 : Real) : HeatPosition)) axis) 0) := rfl
example (readout : HeatDissipationReadout Flow) : readout.IntegralDomainAt =
    ((∀ first second, Integrable (readout.resistancePairingDensityAt first second) readout.volumeMeasure) ∧
      ∀ flow,
        Integrable (readout.entropySupplyDensityAt flow) readout.volumeMeasure ∧
          Integrable (fun position => -readout.divergenceAt flow position / readout.temperatureValueAt position)
            readout.volumeMeasure ∧
          Integrable (fun position => readout.normalFluxAt flow position / readout.temperatureValueAt position)
            readout.boundaryMeasure) := rfl
example (readout : HeatDissipationReadout Flow) : readout.InverseConductivityAt =
    (∀ position, readout.conductivityValueAt position * readout.resistanceValueAt position = 1 ∧
      readout.resistanceValueAt position * readout.conductivityValueAt position = 1) := rfl
example (readout : HeatDissipationReadout Flow) : readout.ReciprocalConductivityAt =
    (∀ position, (readout.conductivityValueAt position).transpose = readout.conductivityValueAt position) := rfl
example (readout : HeatDissipationReadout Flow) : readout.ReciprocalResistanceAt =
    (∀ position, (readout.resistanceValueAt position).transpose = readout.resistanceValueAt position) := rfl
example (readout : HeatDissipationReadout Flow) : readout.PairingIntegralCalculationAt =
    (∀ first second, readout.functionalData.resistancePairing first second =
      ∫ position, readout.resistancePairingDensityAt first second position ∂readout.volumeMeasure) := rfl
example (readout : HeatDissipationReadout Flow) : readout.EntropyIntegralCalculationAt =
    (∀ flow, readout.functionalData.entropySupply flow =
      ∫ position, readout.entropySupplyDensityAt flow position ∂readout.volumeMeasure) := rfl
example (readout : HeatDissipationReadout Flow) : readout.GreenEntropyBalanceAt =
    (∀ flow, readout.systemEntropyRate flow + readout.boundaryEntropyRate flow =
      readout.functionalData.entropySupply flow) := rfl
example (readout : HeatDissipationReadout Flow) (physical : Flow) : readout.PointwiseConstitutiveAt physical =
    (∀ position axis, readout.inverseTemperatureGradientAt position axis =
      (∑ secondAxis, readout.resistanceValueAt position axis secondAxis *
        readout.flowValueAt physical position secondAxis) / readout.temperatureValueAt position) := rfl
example (readout : HeatDissipationReadout Flow) (flow : Flow) : readout.IsolatedAt flow =
    (∀ᵐ position ∂readout.boundaryMeasure, readout.normalFluxAt flow position = 0) := rfl
example (readout : HeatDissipationReadout Flow) (flow : Flow) : readout.StationaryAt flow =
    (∀ᵐ position ∂readout.volumeMeasure, readout.divergenceAt flow position = 0) := rfl
example (readout : HeatDissipationReadout Flow) (prescribed : HeatPosition → Real) (flow : Flow) :
    readout.PrescribedNormalFluxAt prescribed flow =
      (readout.normalFluxAt flow =ᵐ[readout.boundaryMeasure] prescribed) := rfl
example (readout : HeatDissipationReadout Flow) (prescribed : HeatPosition → Real) :
    readout.CompatibleNormalFluxAt prescribed =
      ((∫ position, prescribed position ∂readout.boundaryMeasure) = 0) := rfl
example (readout : HeatDissipationReadout Flow) (flow : Flow) : readout.StationaryPowerConstraintAt flow =
    (readout.StationaryAt flow ∧ readout.boundaryEntropyRate flow =
      2 * readout.functionalData.dissipation flow) := rfl
end SpatialContract